<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Imp: 简单的指令式程序</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Imp<span class="subtitle">简单的指令式程序</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 在本章中，我们会更加认真地看待如何用 Coq 来研究其它东西。
    我们的案例研究是一个名为 Imp 的<b>简单的指令式编程语言</b>，
    它包含了传统主流语言（如 C 和 Java）的一小部分核心片段。下面是一个用
    Imp 编写的常见数学函数：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Z</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">WHILE</span>&nbsp;~(<span class="id" type="var">Z</span>&nbsp;=&nbsp;0)&nbsp;<span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;*&nbsp;<span class="id" type="var">Z</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Z</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">Z</span>&nbsp;-&nbsp;1<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>

 本章关注于如何定义 Imp 的<b>语法</b>和<b>语义</b>；<b>《编程语言基础》
    （Programming Language Foundations）</b>（<b>《软件基础》</b>第二卷）
    中的章节则发展了<b>程序等价关系（Program Equivalence）</b>并引入了
    <b>霍尔逻辑（Hoare Logic）</b>，它是一种广泛用于推理指令式程序的逻辑。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Bool.Bool</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Init.Nat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.Arith</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.EqNat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">omega.Omega</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Lists.List</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Strings.String</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">ListNotations</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Maps</span>.<br/>
</div>

<div class="doc">
<a name="lab320"></a><h1 class="section">算术和布尔表达式</h1>

<div class="paragraph"> </div>

 我们会分三部分来展示 Imp：首先是<b>算术和布尔表达式</b>的核心语言，
    之后是用<b>变量</b>对表达式的扩展，最后是一个包括赋值、条件、串连和循环的
    <b>指令</b>语言。 
</div>

<div class="doc">
<a name="lab321"></a><h2 class="section">语法</h2>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">AExp</span>.<br/>
</div>

<div class="doc">
以下两个定义指定了算术和布尔表达式的<b>抽象语法（Abstract Syntax）</b>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">aexp</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">ANum</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMinus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMult</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">bexp</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">BTrue</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BEq</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BLe</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BNot</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BAnd</span> (<span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> : <span class="id" type="var">bexp</span>).<br/>
</div>

<div class="doc">
在本章中，我们省略了大部分从程序员实际编写的具体语法到其抽象语法树的翻译
 例如，它会将字符串 <span class="inlinecode">"1</span> <span class="inlinecode">+</span> <span class="inlinecode">2</span> <span class="inlinecode">*</span> <span class="inlinecode">3"</span> 翻译成如下 AST：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">APlus</span>&nbsp;(<span class="id" type="var">ANum</span>&nbsp;1)&nbsp;(<span class="id" type="var">AMult</span>&nbsp;(<span class="id" type="var">ANum</span>&nbsp;2)&nbsp;(<span class="id" type="var">ANum</span>&nbsp;3)).
<div class="paragraph"> </div>

</div>
    可选的章节 <a href="ImpParser.html"><span class="inlineref">ImpParser</span></a> 中开发了一个简单的词法分析器和解析器，
    它可以进行这种翻译。你<b>无需</b>通过理解该章来理解本章，
    但如果你没有上过涵盖这些技术的课程（例如编译器课程），可能想要略读一下该章节。 
<div class="paragraph"> </div>

 作为对比，下面是用约定的 BNF（巴克斯-诺尔范式）文法定义的同样的抽象语法：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">a</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">nat</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">a</span>&nbsp;+&nbsp;<span class="id" type="var">a</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">a</span>&nbsp;-&nbsp;<span class="id" type="var">a</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">a</span>&nbsp;*&nbsp;<span class="id" type="var">a</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">b</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">true</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">false</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">a</span>&nbsp;=&nbsp;<span class="id" type="var">a</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">a</span>&nbsp;≤&nbsp;<span class="id" type="var">a</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;¬<span class="id" type="var">b</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">b</span>&nbsp;&amp;&amp;&nbsp;<span class="id" type="var">b</span>
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>

 与前面的 Coq 版本相对比...

<div class="paragraph"> </div>

<ul class="doclist">
<li> BNF 是非形式化的 &mdash; 例如，它给出了表达式表面上的语法的建议
         （例如加法运算符写作中缀的 <span class="inlinecode">+</span>），而没有指定词法分析和解析的其它方面
         （如 <span class="inlinecode">+</span>、<span class="inlinecode">-</span> 和 <span class="inlinecode">*</span> 的相对优先级，用括号来明确子表达式的分组等）。
         在实现编译器时，需要一些附加的信息（以及人类的智慧）
         才能将此描述转换成形式化的定义。

<div class="paragraph"> </div>

         Coq 版本则始终忽略了所有这些信息，只专注于抽象语法。

<div class="paragraph"> </div>


</li>
<li> 反之，BNF 版本则更加清晰易读。它的非形式化使其更加灵活，
         在讨论和在黑板上书写时，它有很大的优势，
         此时传达一般的概念要比精确定下所有细节更加重要。

<div class="paragraph"> </div>

         确实，存在很多种类似 BNF 的记法，人们可以随意使用它们，
         而无需关心具体使用了哪种 BNF，因为没有必要：
         大致的理解是非常重要的。

</li>
</ul>

<div class="paragraph"> </div>

    适应这两种记法都很有必要：非形式化的用语人类之间的交流，
    而形式化的则用于实现和证明。 
</div>

<div class="doc">
<a name="lab322"></a><h2 class="section">求值</h2>

<div class="paragraph"> </div>

 对算术表达式进行<b>求值（Evaluation）</b>会得到数值。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">aeval</span> (<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>) : <span class="id" type="var">nat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">a</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ANum</span> <span class="id" type="var">n</span> ⇒ <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span>  <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">a<sub>1</sub></span>) + (<span class="id" type="var">aeval</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">a<sub>1</sub></span>) - (<span class="id" type="var">aeval</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMult</span>  <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">a<sub>1</sub></span>) * (<span class="id" type="var">aeval</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_aeval1</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">aeval</span> (<span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 2) (<span class="id" type="var">ANum</span> 2)) = 4.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
同样，对布尔表达式求值会得到布尔值。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">beval</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) : <span class="id" type="var">bool</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">b</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BTrue</span>       ⇒ <span class="id" type="var">true</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BFalse</span>      ⇒ <span class="id" type="var">false</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BEq</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>   ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">a<sub>1</sub></span>) =? (<span class="id" type="var">aeval</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BLe</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>   ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">a<sub>1</sub></span>) &lt;=? (<span class="id" type="var">aeval</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BNot</span> <span class="id" type="var">b<sub>1</sub></span>     ⇒ <span class="id" type="var">negb</span> (<span class="id" type="var">beval</span> <span class="id" type="var">b<sub>1</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BAnd</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span>  ⇒ <span class="id" type="var">andb</span> (<span class="id" type="var">beval</span> <span class="id" type="var">b<sub>1</sub></span>) (<span class="id" type="var">beval</span> <span class="id" type="var">b<sub>2</sub></span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
<a name="lab323"></a><h2 class="section">优化</h2>

<div class="paragraph"> </div>

 我们尚未定义太多东西，不过从这些定义出发，已经能前进不少了。
    假设我们定义了一个接收算术表达式并对它稍微进行化简的函数，即将所有的
    <span class="inlinecode">0</span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">e</span></span>（如 <span class="inlinecode">(<span class="id" type="var">APlus</span></span> <span class="inlinecode">(<span class="id" type="var">ANum</span></span> <span class="inlinecode">0)</span> <span class="inlinecode"><span class="id" type="var">e</span></span>）化简为 <span class="inlinecode"><span class="id" type="var">e</span></span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">optimize_0plus</span> (<span class="id" type="var">a</span>:<span class="id" type="var">aexp</span>) : <span class="id" type="var">aexp</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">a</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ANum</span> <span class="id" type="var">n</span> ⇒ <span class="id" type="var">ANum</span> <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 0) <span class="id" type="var">e<sub>2</sub></span> ⇒ <span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span>  <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span> ⇒ <span class="id" type="var">APlus</span>  (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e<sub>1</sub></span>) (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMinus</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span> ⇒ <span class="id" type="var">AMinus</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e<sub>1</sub></span>) (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMult</span>  <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span> ⇒ <span class="id" type="var">AMult</span>  (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e<sub>1</sub></span>) (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">e<sub>2</sub></span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
要保证我们的优化是正确的，可以在某些示例中测试它并观察其输出出否正确。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_optimize_0plus</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">optimize_0plus</span> (<span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 2)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 0)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 0) (<span class="id" type="var">ANum</span> 1))))<br/>
&nbsp;&nbsp;= <span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 2) (<span class="id" type="var">ANum</span> 1).<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
但如果要确保该优化的正确性，即优化后的表达式与原表达式的求值结果相同，
    那么我们应当证明它。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">optimize_0plus_sound</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">aeval</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">a</span>) = <span class="id" type="var">aeval</span> <span class="id" type="var">a</span>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;ANum&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;APlus&nbsp;*)</span> <span class="id" type="tactic">destruct</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Ea<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;a<sub>1</sub>&nbsp;=&nbsp;ANum&nbsp;n&nbsp;*)</span> <span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">En</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;n&nbsp;=&nbsp;0&nbsp;*)</span>  <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHa2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;n&nbsp;&lt;&gt;&nbsp;0&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;a<sub>1</sub>&nbsp;=&nbsp;APlus&nbsp;a1_1&nbsp;a1_2&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;a<sub>1</sub>&nbsp;=&nbsp;AMinus&nbsp;a1_1&nbsp;a1_2&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;a<sub>1</sub>&nbsp;=&nbsp;AMult&nbsp;a1_1&nbsp;a1_2&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;AMinus&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;AMult&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab324"></a><h1 class="section">Coq 自动化</h1>

<div class="paragraph"> </div>

 上一个证明中的大量重复很让人烦躁。无论算术表达式的语言，
    还是证明优化的可靠性明显都更加复杂，因此它会成为一个真正的问题。

<div class="paragraph"> </div>

    目前为止，我们所有的证明都只使用了一点趁手的 Coq 的策略，
    而它自动构造部分证明的强大功能则完全被忽略了。本节引入了这样的一些功能，
    而在下一章中我们会看到更多。要使用它们需要耗费点精力 &mdash;
    Coq 的自动化是个强大的工具 &mdash; 不过它能让我们从无聊、重复、
    底层的细节中解放出来，专注于更加复杂的定义和更加有趣的性质。 
</div>

<div class="doc">
<a name="lab325"></a><h2 class="section">泛策略</h2>

<div class="paragraph"> </div>

 <b>泛策略（Tacticals）</b>是 Coq 中的术语，它表示一个接受其它策略作为参数的策略，
    当然，你愿意的话也可以把它称为“高阶策略”。 
</div>

<div class="doc">
<a name="lab326"></a><h3 class="section"><span class="inlinecode"><span class="id" type="tactic">try</span></span> 泛策略</h3>

<div class="paragraph"> </div>

 如果 <span class="inlinecode"><span class="id" type="var">T</span></span> 是一个策略，那么 <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> 是一个和 <span class="inlinecode"><span class="id" type="var">T</span></span> 一样的策略，只是如果
    <span class="inlinecode"><span class="id" type="var">T</span></span> 失败的话，<span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> 就会<b>成功地</b>什么也不做（而非失败）。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">silly1</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">ae</span>, <span class="id" type="var">aeval</span> <span class="id" type="var">ae</span> = <span class="id" type="var">aeval</span> <span class="id" type="var">ae</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>. <span class="comment">(*&nbsp;它和&nbsp;<span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span>&nbsp;做的一样。&nbsp;*)</span> <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">silly2</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="keyword">Prop</span>), <span class="id" type="var">P</span> → <span class="id" type="var">P</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">HP</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>. <span class="comment">(*&nbsp;和&nbsp;<span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span>&nbsp;失败时一样。&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">HP</span>. <span class="comment">(*&nbsp;我们仍然可以换种方式来结束此证明。&nbsp;*)</span><br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
我们并没有真正的理由在像这样的手动证明中使用 <span class="inlinecode"><span class="id" type="tactic">try</span></span>，不过在连同
    <span class="inlinecode">;</span> 泛策略一起进行自动化证明时它会非常有用，接下来我们来展示它。 
</div>

<div class="doc">
<a name="lab327"></a><h3 class="section"><span class="inlinecode">;</span> 泛策略（简单形式）</h3>

<div class="paragraph"> </div>

 在最常用的形式中，<span class="inlinecode">;</span> 泛策略会接受两个策略作为参数。复合策略 <span class="inlinecode"><span class="id" type="var">T</span>;<span class="id" type="var">T'</span></span>
    会在 <span class="inlinecode"><span class="id" type="var">T</span></span> 生成的<b>每个子目标</b>中先执行 <span class="inlinecode"><span class="id" type="var">T</span></span> 再执行 <span class="inlinecode"><span class="id" type="var">T'</span></span>。 
<div class="paragraph"> </div>

 例如，考虑以下平凡的引理： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">foo</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, 0 &lt;=? <span class="id" type="var">n</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;会产生两个执行过程相同的子目标...&nbsp;&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;n=0&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;n=Sn'&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
我们可以用 <span class="inlinecode">;</span> 泛策略来化简它： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">foo'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, 0 &lt;=? <span class="id" type="var">n</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;<span class="inlinecode"><span class="id" type="tactic">destruct</span></span>&nbsp;解构当前子目标&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span>;<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;然后用&nbsp;<span class="inlinecode"><span class="id" type="tactic">simpl</span></span>&nbsp;化简每个产生的子目标&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>;<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;之后再对每个产生的子目标执行&nbsp;<span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="tactic">try</span></span> 配合 <span class="inlinecode">;</span> 一同使用，我们可以从之前证明中麻烦的重复里解脱出来。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">optimize_0plus_sound'</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">aeval</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">a</span>) = <span class="id" type="var">aeval</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;大部分情况后面直接就是&nbsp;IH...&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> (<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;...&nbsp;不过剩下的情况&nbsp;--&nbsp;ANum&nbsp;和&nbsp;APlus&nbsp;--&nbsp;则不同：&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;ANum&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;APlus&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Ea<sub>1</sub></span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;同样，大部分情况后面直接就是&nbsp;IH：&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> (<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;当&nbsp;<span class="inlinecode"><span class="id" type="var">e<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>&nbsp;时出现了有趣的情况，其中&nbsp;<span class="inlinecode"><span class="id" type="tactic">try</span>...</span>&nbsp;什么也不做。<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;此时，我们需要解构&nbsp;<span class="inlinecode"><span class="id" type="var">n</span></span>（来确认优化是否应用）并用归纳假设来改写它。&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;a<sub>1</sub>&nbsp;=&nbsp;ANum&nbsp;n&nbsp;*)</span> <span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">En</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Coq 专家经常在像 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 这样的策略之后使用这种“<span class="inlinecode">...;</span> <span class="inlinecode"><span class="id" type="tactic">try</span>...</span> <span class="inlinecode"></span>”的习语，
    以便一次处理所有相似的情况。自然，在非形式化证明中也有同样的做法。
    例如，以下对该优化定理的非形式化证明与形式化证明的结构一致：

<div class="paragraph"> </div>

    <b>定理</b>：对于所有的算术表达式 <span class="inlinecode"><span class="id" type="var">a</span></span>，

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aeval</span>&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">a</span>)&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">a</span>.
<div class="paragraph"> </div>

</div>
    <b>证明</b>：对 <span class="inlinecode"><span class="id" type="var">a</span></span> 进行归纳。大部分情况根据即可 IH 得证。其余情况如下：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 假设设对于某些 <span class="inlinecode"><span class="id" type="var">n</span></span> 有 <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> for some <span class="inlinecode"><span class="id" type="var">n</span></span>。我们必须证明

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">aeval</span>&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;(<span class="id" type="var">ANum</span>&nbsp;<span class="id" type="var">n</span>))&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;(<span class="id" type="var">ANum</span>&nbsp;<span class="id" type="var">n</span>).
<div class="paragraph"> </div>

</div>
        这一点根据 <span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span> 的定义即可得证。

<div class="paragraph"> </div>


</li>
<li> 假设对于某些 <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span> 有 <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">APlus</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span>。我们必须证明

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">aeval</span>&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;(<span class="id" type="var">APlus</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>))&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;(<span class="id" type="var">APlus</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>).
<div class="paragraph"> </div>

</div>
        考虑 <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> 可能的形式。对于大部分的情况，<span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span>
        会对子表达式简单地递归调用自身并重建一个与 <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> 形式相同的新表达式；
        在这些情况下，其结果根据 IH 即可得证。

<div class="paragraph"> </div>

        对某些 <span class="inlinecode"><span class="id" type="var">n</span></span> 有 <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 是个有趣的情况。若 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>，则

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">optimize_0plus</span>&nbsp;(<span class="id" type="var">APlus</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)&nbsp;=&nbsp;<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>
<div class="paragraph"> </div>

</div>
        而 <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span> 的 IH 正是所需的。另一方面，如果对于某些 <span class="inlinecode"><span class="id" type="var">n'</span></span> 有 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>
        那么同样 <span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span> 会简单地递归调用自身，而其结果根据
        IH 即可得证。 <span class="proofbox">&#9744;</span> 
</li>
</ul>

<div class="paragraph"> </div>

 然而，此证明仍然可以改进：第一种情况（<span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>）非常平凡，
    甚至比我们根据归纳假设化简的那个情况还要平凡，然而我们却把它完整地写了出来。
    为了更加清楚，最好把它去掉，然后在最上面说：“大部分情况可以立即得出，
    或直接从归纳假设得出。唯一有趣的情况是 <span class="inlinecode"><span class="id" type="var">APlus</span></span>...”
    我们也可以在形式化证明中做出这种改进，方法如下： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">optimize_0plus_sound''</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">aeval</span> (<span class="id" type="var">optimize_0plus</span> <span class="id" type="var">a</span>) = <span class="id" type="var">aeval</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Most&nbsp;cases&nbsp;follow&nbsp;directly&nbsp;by&nbsp;the&nbsp;IH&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> (<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;...&nbsp;or&nbsp;are&nbsp;immediate&nbsp;by&nbsp;definition&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;interesting&nbsp;case&nbsp;is&nbsp;when&nbsp;a&nbsp;=&nbsp;APlus&nbsp;a<sub>1</sub>&nbsp;a<sub>2</sub>.&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;APlus&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">a<sub>1</sub></span>; <span class="id" type="tactic">try</span> (<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;a<sub>1</sub>&nbsp;=&nbsp;ANum&nbsp;n&nbsp;*)</span> <span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab328"></a><h3 class="section"><span class="inlinecode">;</span> 泛策略（一般形式）</h3>

<div class="paragraph"> </div>

 <span class="inlinecode">;</span> 除了我们前面见到的简单形式 <span class="inlinecode"><span class="id" type="var">T</span>;<span class="id" type="var">T'</span></span> 外，还有种更一般的形式。
    如果 <span class="inlinecode"><span class="id" type="var">T</span></span>, <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span>, ..., <span class="inlinecode"><span class="id" type="var">Tn</span></span> 都是策略，那么

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">T</span>;&nbsp;[<span class="id" type="var">T<sub>1</sub></span>&nbsp;|&nbsp;<span class="id" type="var">T<sub>2</sub></span>&nbsp;|&nbsp;... |&nbsp;<span class="id" type="var">Tn</span>]
<div class="paragraph"> </div>

</div>
   就是一个首先执行 <span class="inlinecode"><span class="id" type="var">T</span></span>，然后在 <span class="inlinecode"><span class="id" type="var">T</span></span> 生成的第一个字母表中执行 <span class="inlinecode"><span class="id" type="var">T<sub>1</sub></span></span>，
   在第二个子目标中执行 <span class="inlinecode"><span class="id" type="var">T<sub>2</sub></span></span>，以此类推。

<div class="paragraph"> </div>

   因此，<span class="inlinecode"><span class="id" type="var">T</span>;<span class="id" type="var">T'</span></span> 只是一种当所有 <span class="inlinecode"><span class="id" type="var">Ti</span></span> 为相同策略时的特殊记法，即，<span class="inlinecode"><span class="id" type="var">T</span>;<span class="id" type="var">T'</span></span>
   是以下形式的简写：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">T</span>;&nbsp;[<span class="id" type="var">T'</span>&nbsp;|&nbsp;<span class="id" type="var">T'</span>&nbsp;|&nbsp;... |&nbsp;<span class="id" type="var">T'</span>]
<div class="paragraph"> </div>

</div>

</div>

<div class="doc">
<a name="lab329"></a><h3 class="section"><span class="inlinecode"><span class="id" type="tactic">repeat</span></span> 泛策略</h3>

<div class="paragraph"> </div>

 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> 泛策略接受另一个测略并重复应用它直至失败。以下示例用
    <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> 证明了 <span class="inlinecode">10</span> 在一个长列表中。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">In<sub>10</sub></span> : <span class="id" type="var">In</span> 10 [1;2;3;4;5;6;7;8;9;10].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">repeat</span> (<span class="id" type="tactic">try</span> (<span class="id" type="var">left</span>; <span class="id" type="tactic">reflexivity</span>); <span class="id" type="var">right</span>).<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
策略 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> 永远不会失败：如果策略 <span class="inlinecode"><span class="id" type="var">T</span></span> 并未应用到原始目标上，
    那么 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> 仍然会成功而不改变原始目标（即，它重复了零次）。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">In<sub>10</sub>'</span> : <span class="id" type="var">In</span> 10 [1;2;3;4;5;6;7;8;9;10].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">repeat</span> (<span class="id" type="var">left</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">repeat</span> (<span class="id" type="var">right</span>; <span class="id" type="tactic">try</span> (<span class="id" type="var">left</span>; <span class="id" type="tactic">reflexivity</span>)).<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
策略 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> 应用 <span class="inlinecode"><span class="id" type="var">T</span></span> 的次数也没有任何上界。如果 <span class="inlinecode"><span class="id" type="var">T</span></span> 策略总是成功，
    那么重复 <span class="inlinecode"><span class="id" type="var">T</span></span> 会永远循环（例如 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> 会一直循环，因为 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span>
    总是会成功）。虽然 Coq 的主语言 Gallina 中的求值保证会终止，
    然而策略却不会！然而这并不会影响 Coq 的逻辑一致性，因为 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span>
    和其它策略的工作就是指导 Coq 去构造证明；如果构造过程发散（即不停机），
    那就意味着我们构造证明失败，而非构造出了错误的证明。 
<div class="paragraph"> </div>

<a name="lab330"></a><h4 class="section">练习：3 星, standard (optimize_0plus_b_sound)</h4>
 由于 <span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span> 变换不会改变 <span class="inlinecode"><span class="id" type="var">aexp</span></span> 的值，
    因此我们可以将它应用到所有出现在 <span class="inlinecode"><span class="id" type="var">bexp</span></span> 中的 <span class="inlinecode"><span class="id" type="var">aexp</span></span> 上而不改变
    <span class="inlinecode"><span class="id" type="var">bexp</span></span> 的值。请编写一个对 <span class="inlinecode"><span class="id" type="var">bexp</span></span> 执行此变换的函数，并证明它的可靠性。
    利用我们刚学过的泛策略来构造一个尽可能优雅的证明。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">optimize_0plus_b</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) : <span class="id" type="var">bexp</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">optimize_0plus_b_sound</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">beval</span> (<span class="id" type="var">optimize_0plus_b</span> <span class="id" type="var">b</span>) = <span class="id" type="var">beval</span> <span class="id" type="var">b</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab331"></a><h4 class="section">练习：4 星, standard, optional (optimize)</h4>
 <b>设计练习</b>：<span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span> 函数只是众多算术和布尔表达式优化的方法之一。
    请编写一个更加聪明的优化器并证明它的正确性。（最容易的方法就是从小处着手：
    一开始只添加单个简单的优化并证明它的正确性，然后逐渐增加其它更有趣的优化。） 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab332"></a><h2 class="section">定义新的策略记法</h2>

<div class="paragraph"> </div>

 Coq 还提供了几种对策略脚本进行“编程”的方式。

<div class="paragraph"> </div>

<ul class="doclist">
<li> 下面展示的 <span class="inlinecode"><span class="id" type="keyword">Tactic</span></span> <span class="inlinecode"><span class="id" type="keyword">Notation</span></span> 习语给出了定义“简写策略”的简便方式，
      它将多个策略封装成单条指令。

<div class="paragraph"> </div>


</li>
<li> 对于更加复杂的编程，Coq 提供了内建的 <span class="inlinecode"><span class="id" type="keyword">Ltac</span></span> 语言，
      它带有可以检查和修改证明状态的原语。由于详情太过复杂，这里不便展开
      （<span class="inlinecode"><span class="id" type="keyword">Ltac</span></span> 通常也被认为不是 Coq 的设计中最美妙的部分！），
      你可以在参考手册和其它关于 Coq 的书中找到它，Coq 的标准库中有很多
      <span class="inlinecode"><span class="id" type="keyword">Ltac</span></span> 定义的例子，你也可以参考它们。

<div class="paragraph"> </div>


</li>
<li> 还有 OCaml 的 API，它可以构建从底层访问 Coq 内部结构的策略，
      不过普通 Coq 用于很少需要麻烦它。

</li>
</ul>
    <span class="inlinecode"><span class="id" type="keyword">Tactic</span></span> <span class="inlinecode"><span class="id" type="keyword">Notation</span></span> 机制是最易于掌握的，它为很多用途提供了强大的能力。
    下面就是个例子。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Tactic Notation</span> "simpl_and_try" <span class="id" type="var">tactic</span>(<span class="id" type="var">c</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>;<br/>
&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="var">c</span>.<br/>
</div>

<div class="doc">
这定义了一个新的名为 <span class="inlinecode"><span class="id" type="var">simpl_and_try</span></span> 的泛策略，它接受一个策略 <span class="inlinecode"><span class="id" type="var">c</span></span>
    作为参数，其定义等价于策略 <span class="inlinecode"><span class="id" type="tactic">simpl</span>;</span> <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span>。现在在证明中写
    “<span class="inlinecode"><span class="id" type="var">simpl_and_try</span></span> <span class="inlinecode"><span class="id" type="tactic">reflexivity</span>.</span>”和写“<span class="inlinecode"><span class="id" type="tactic">simpl</span>;</span> <span class="inlinecode"><span class="id" type="tactic">try</span></span> <span class="inlinecode"><span class="id" type="tactic">reflexivity</span>.</span>”是一样的。 
</div>

<div class="doc">
<a name="lab333"></a><h2 class="section"><span class="inlinecode"><span class="id" type="tactic">omega</span></span> 策略</h2>

<div class="paragraph"> </div>

 <span class="inlinecode"><span class="id" type="tactic">omega</span></span> 实现了一种决策过程，它是名为<b>Presburger 算术</b>的一阶逻辑的一个子集。
    它基于启发自 William Pugh <a href="Bib.html#Pugh 1991"><span class="inlineref">[Pugh 1991]</span></a> 的 Omega 算法。

<div class="paragraph"> </div>

    如果证明目标是由以下元素构成的式子：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 数值常量、加法（<span class="inlinecode">+</span> 和 <span class="inlinecode"><span class="id" type="var">S</span></span>）、减法（<span class="inlinecode">-</span> 和 <span class="inlinecode"><span class="id" type="var">pred</span></span>）以及常量乘法
        （这就是 Presburger 算术的构成要素）

<div class="paragraph"> </div>


</li>
<li> 相等关系（<span class="inlinecode">=</span> 和 <span class="inlinecode">≠</span>）和序（<span class="inlinecode">≤</span>）

<div class="paragraph"> </div>


</li>
<li> 逻辑连结 <span class="inlinecode">∧</span>、<span class="inlinecode">∨</span>、<span class="inlinecode">¬</span> 和 <span class="inlinecode">→</span>

</li>
</ul>

<div class="paragraph"> </div>

    那么调用 <span class="inlinecode"><span class="id" type="tactic">omega</span></span> 要么会解决该证明目标，要么就会失败，这意味着该目标为假
    （目标<b>不满足</b>此形式也会失败。） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">silly_presburger_example</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> <span class="id" type="var">p</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">m</span> + <span class="id" type="var">n</span> ≤ <span class="id" type="var">n</span> + <span class="id" type="var">o</span> ∧ <span class="id" type="var">o</span> + 3 = <span class="id" type="var">p</span> + 3 →<br/>
&nbsp;&nbsp;<span class="id" type="var">m</span> ≤ <span class="id" type="var">p</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
（注意本文件顶部 <span class="inlinecode"><span class="id" type="var">From</span></span> <span class="inlinecode"><span class="id" type="var">Coq</span></span> <span class="inlinecode"><span class="id" type="keyword">Require</span></span> <span class="inlinecode"><span class="id" type="keyword">Import</span></span> <span class="inlinecode"><span class="id" type="var">omega.Omega</span>.</span>。）
</div>

<div class="doc">
<a name="lab334"></a><h2 class="section">更多方便的策略</h2>

<div class="paragraph"> </div>

 最后，下面列出一些方便的其它技巧。

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="tactic">clear</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>：从上下文中删除前提 <span class="inlinecode"><span class="id" type="var">H</span></span>。

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">subst</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>：对于变量 <span class="inlinecode"><span class="id" type="var">x</span></span>，在上下文中查找假设 <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">e</span></span> 或 <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">x</span></span>，
       将整个上下文和当前目标中的所有 <span class="inlinecode"><span class="id" type="var">x</span></span> 替换为 <span class="inlinecode"><span class="id" type="var">e</span></span> 并清除该假设。

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">subst</span></span>：替换掉<b>所有</b>形如 <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">e</span></span> 或 <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">x</span></span> 的假设（其中 <span class="inlinecode"><span class="id" type="var">x</span></span> 为变量）。

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">rename</span>...</span> <span class="inlinecode"><span class="id" type="var">into</span>...</span>：更改证明上下文中前提的名字。例如，
       如果上下文中包含名为 <span class="inlinecode"><span class="id" type="var">x</span></span> 的变量，那么 <span class="inlinecode"><span class="id" type="tactic">rename</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">into</span></span> <span class="inlinecode"><span class="id" type="var">y</span></span>
       就会将所有出现的 <span class="inlinecode"><span class="id" type="var">x</span></span> 重命名为 <span class="inlinecode"><span class="id" type="var">y</span></span>。

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="tactic">assumption</span></span>：尝试在上下文中查找完全匹配目标的前提 <span class="inlinecode"><span class="id" type="var">H</span></span>。
       如果找到了，那么其行为与 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> 相同。

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="var">contradiction</span></span>：尝试在当前上下文中查找逻辑等价于 <span class="inlinecode"><span class="id" type="var">False</span></span> 的前提 <span class="inlinecode"><span class="id" type="var">H</span></span>。
      如果找到了，就解决该目标。

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="var">constructor</span></span>：尝试在当前环境中的 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span>
       定义中查找可用于解决当前目标的构造子 <span class="inlinecode"><span class="id" type="var">c</span></span>。如果找到了，那么其行为与
       <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> 相同。

</li>
</ul>

<div class="paragraph"> </div>

    我们之后会看到所有它们的例子。 
</div>

<div class="doc">
<a name="lab335"></a><h1 class="section">求值作为关系</h1>

<div class="paragraph"> </div>

 我们已经展示了用 <span class="inlinecode"><span class="id" type="keyword">Fixpoint</span></span> 定义的函数 <span class="inlinecode"><span class="id" type="var">aeval</span></span> 和 <span class="inlinecode"><span class="id" type="var">beval</span></span>。
    另一种通常更加灵活的思考求值的方式，就是把它当做表达式与其值的<b>关系</b>。
    （译注：求值关系不满足对称性，因为它是有方向的。）
    这会自然地导出如下这种算术表达式的 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 定义... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">aevalR_first_try</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">aevalR</span> : <span class="id" type="var">aexp</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_ANum</span> <span class="id" type="var">n</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> (<span class="id" type="var">ANum</span> <span class="id" type="var">n</span>) <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_APlus</span> (<span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>: <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span>: <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">n<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">n<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> (<span class="id" type="var">APlus</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>) (<span class="id" type="var">n<sub>1</sub></span> + <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_AMinus</span> (<span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>: <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span>: <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">n<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">n<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> (<span class="id" type="var">AMinus</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>) (<span class="id" type="var">n<sub>1</sub></span> - <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_AMult</span> (<span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>: <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span>: <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">n<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">n<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> (<span class="id" type="var">AMult</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>) (<span class="id" type="var">n<sub>1</sub></span> * <span class="id" type="var">n<sub>2</sub></span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">TooHardToRead</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;A&nbsp;small&nbsp;notational&nbsp;aside.&nbsp;We&nbsp;would&nbsp;previously&nbsp;have&nbsp;written&nbsp;the<br/>
&nbsp;&nbsp;&nbsp;definition&nbsp;of&nbsp;<span class="inlinecode"><span class="id" type="var">aevalR</span></span>&nbsp;like&nbsp;this,&nbsp;with&nbsp;explicit&nbsp;names&nbsp;for&nbsp;the<br/>
&nbsp;&nbsp;&nbsp;hypotheses&nbsp;in&nbsp;each&nbsp;case:&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">aevalR</span> : <span class="id" type="var">aexp</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_ANum</span> <span class="id" type="var">n</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> (<span class="id" type="var">ANum</span> <span class="id" type="var">n</span>) <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_APlus</span> (<span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>: <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span>: <span class="id" type="var">nat</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>1</sub></span> : <span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">n<sub>1</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>2</sub></span> : <span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">n<sub>2</sub></span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> (<span class="id" type="var">APlus</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>) (<span class="id" type="var">n<sub>1</sub></span> + <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_AMinus</span> (<span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>: <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span>: <span class="id" type="var">nat</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>1</sub></span> : <span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">n<sub>1</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>2</sub></span> : <span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">n<sub>2</sub></span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> (<span class="id" type="var">AMinus</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>) (<span class="id" type="var">n<sub>1</sub></span> - <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_AMult</span> (<span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>: <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span>: <span class="id" type="var">nat</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>1</sub></span> : <span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">n<sub>1</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>2</sub></span> : <span class="id" type="var">aevalR</span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">n<sub>2</sub></span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span> (<span class="id" type="var">AMult</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>) (<span class="id" type="var">n<sub>1</sub></span> * <span class="id" type="var">n<sub>2</sub></span>).<br/>
</div>

<div class="doc">
Instead, we've chosen to leave the hypotheses anonymous, just
    giving their types.  This style gives us less control over the
    names that Coq chooses during proofs involving <span class="inlinecode"><span class="id" type="var">aevalR</span></span>, but it
    makes the definition itself quite a bit lighter. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">TooHardToRead</span>.<br/>
</div>

<div class="doc">
如果 <span class="inlinecode"><span class="id" type="var">aevalR</span></span> 有中缀记法的话会很方便。我们用 <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode">\\</span> <span class="inlinecode"><span class="id" type="var">n</span></span>
    表示算术表达式 <span class="inlinecode"><span class="id" type="var">e</span></span> 求值为 <span class="inlinecode"><span class="id" type="var">n</span></span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Notation</span> "e '\\' n"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= (<span class="id" type="var">aevalR</span> <span class="id" type="var">e</span> <span class="id" type="var">n</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 50, <span class="id" type="var">left</span> <span class="id" type="var">associativity</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">type_scope</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">aevalR_first_try</span>.<br/>
</div>

<div class="doc">
实际上，Coq 提供了一种在 <span class="inlinecode"><span class="id" type="var">aevalR</span></span> 自身内使用此记法的方式。
    这样可以避免在进行涉及 <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode">\\</span> <span class="inlinecode"><span class="id" type="var">n</span></span> 形式的证明时，必须向前引用
    <span class="inlinecode"><span class="id" type="var">aevalR</span></span> <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 形式的定义的情况，从而减少混淆。

<div class="paragraph"> </div>

    具体做法是，我们先“保留”该记法，然后在给出定义的同时声明它的意义。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Reserved Notation</span> "e '\\' n" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 90, <span class="id" type="var">left</span> <span class="id" type="var">associativity</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">aevalR</span> : <span class="id" type="var">aexp</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_ANum</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">ANum</span> <span class="id" type="var">n</span>) \\ <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_APlus</span> (<span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">e<sub>1</sub></span> \\ <span class="id" type="var">n<sub>1</sub></span>) → (<span class="id" type="var">e<sub>2</sub></span> \\ <span class="id" type="var">n<sub>2</sub></span>) → (<span class="id" type="var">APlus</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>) \\ (<span class="id" type="var">n<sub>1</sub></span> + <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_AMinus</span> (<span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">e<sub>1</sub></span> \\ <span class="id" type="var">n<sub>1</sub></span>) → (<span class="id" type="var">e<sub>2</sub></span> \\ <span class="id" type="var">n<sub>2</sub></span>) → (<span class="id" type="var">AMinus</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>) \\ (<span class="id" type="var">n<sub>1</sub></span> - <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_AMult</span> (<span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">e<sub>1</sub></span> \\ <span class="id" type="var">n<sub>1</sub></span>) → (<span class="id" type="var">e<sub>2</sub></span> \\ <span class="id" type="var">n<sub>2</sub></span>) → (<span class="id" type="var">AMult</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>) \\ (<span class="id" type="var">n<sub>1</sub></span> * <span class="id" type="var">n<sub>2</sub></span>)<br/>
<br/>
&nbsp;&nbsp;<span class="id" type="keyword">where</span> "e '\\' n" := (<span class="id" type="var">aevalR</span> <span class="id" type="var">e</span> <span class="id" type="var">n</span>) : <span class="id" type="var">type_scope</span>.<br/>
</div>

<div class="doc">
<a name="lab336"></a><h2 class="section">推理规则的记法</h2>

<div class="paragraph"> </div>

 在非形式化的讨论中，将 <span class="inlinecode"><span class="id" type="var">aevalR</span></span> 和类似的关系写成更加易读的
    <b>推理规则（Inference Rule）</b>的图像形式会十分方便，
    其中横线上方的前提证明了横线下方的结论是正确的（我们已经在
    <a href="IndProp.html"><span class="inlineref">IndProp</span></a> 一章中见过它们了）。 
<div class="paragraph"> </div>

 例如，构造子 <span class="inlinecode"><span class="id" type="var">E_APlus</span></span>...

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">E_APlus</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">e<sub>1</sub></span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>:&nbsp;<span class="id" type="var">aexp</span>)&nbsp;(<span class="id" type="var">n<sub>1</sub></span>&nbsp;<span class="id" type="var">n<sub>2</sub></span>:&nbsp;<span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>&nbsp;<span class="id" type="var">n<sub>2</sub></span>&nbsp;→<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aevalR</span>&nbsp;(<span class="id" type="var">APlus</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>)&nbsp;(<span class="id" type="var">n<sub>1</sub></span>&nbsp;+&nbsp;<span class="id" type="var">n<sub>2</sub></span>)
<div class="paragraph"> </div>

</div>
    ...的推理规则写作：
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">e<sub>1</sub>&nbsp;\\&nbsp;n<sub>1</sub></td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">e<sub>2</sub>&nbsp;\\&nbsp;n<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (E_APlus) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">APlus&nbsp;e<sub>1</sub>&nbsp;e<sub>2</sub>&nbsp;\\&nbsp;n<sub>1</sub>+n<sub>2</sub></td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

 形式上来说，推理规则没什么深刻的含义：它们只是蕴含关系。
    你可以将右侧的规则名看做构造子名，将横线上每个前提见的换行（以及横线本身）
    看做 <span class="inlinecode">→</span>。规则中涉及的所有变量（如 <span class="inlinecode"><span class="id" type="var">e<sub>1</sub></span></span>、<span class="inlinecode"><span class="id" type="var">n<sub>1</sub></span></span> 等）从一开始都是全称量化的。
    （这种变量通常称为<b>元变量（Metavariables）</b>，以区别于我们在语言中定义的变量。
    目前，我们的算术表达式中还不包含变量，不过之后会加入它们。）
    整个规则集合都被认为包裹在 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 声明中。在非正式的叙述中，
    这一点要么会忽略，要么会通过类似于“令 <span class="inlinecode"><span class="id" type="var">aevalR</span></span> 为对以下规则封闭的最小关系...”
    的句子来表述。 
<div class="paragraph"> </div>

 例如，<span class="inlinecode">\\</span> 是对以下规则封闭的最小关系：
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (E_ANum) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">ANum&nbsp;n&nbsp;\\&nbsp;n</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">e<sub>1</sub>&nbsp;\\&nbsp;n<sub>1</sub></td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">e<sub>2</sub>&nbsp;\\&nbsp;n<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (E_APlus) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">APlus&nbsp;e<sub>1</sub>&nbsp;e<sub>2</sub>&nbsp;\\&nbsp;n<sub>1</sub>+n<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">e<sub>1</sub>&nbsp;\\&nbsp;n<sub>1</sub></td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">e<sub>2</sub>&nbsp;\\&nbsp;n<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (E_AMinus) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">AMinus&nbsp;e<sub>1</sub>&nbsp;e<sub>2</sub>&nbsp;\\&nbsp;n<sub>1</sub>-n<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">e<sub>1</sub>&nbsp;\\&nbsp;n<sub>1</sub></td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">e<sub>2</sub>&nbsp;\\&nbsp;n<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (E_AMult) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">AMult&nbsp;e<sub>1</sub>&nbsp;e<sub>2</sub>&nbsp;\\&nbsp;n<sub>1</sub>*n<sub>2</sub></td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

<a name="lab337"></a><h4 class="section">练习：1 星, standard, optional (beval_rules)</h4>
 下面是 Coq 中 <span class="inlinecode"><span class="id" type="var">beval</span></span> 函数的定义：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="keyword">Fixpoint</span>&nbsp;<span class="id" type="var">beval</span>&nbsp;(<span class="id" type="var">e</span>&nbsp;:&nbsp;<span class="id" type="var">bexp</span>)&nbsp;:&nbsp;<span class="id" type="var">bool</span>&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span>&nbsp;<span class="id" type="var">e</span>&nbsp;<span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">BTrue</span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;⇒&nbsp;<span class="id" type="var">true</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">BFalse</span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;⇒&nbsp;<span class="id" type="var">false</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>&nbsp;&nbsp;&nbsp;⇒&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)&nbsp;=?&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">BLe</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>&nbsp;&nbsp;&nbsp;⇒&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)&nbsp;&lt;=?&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">BNot</span>&nbsp;<span class="id" type="var">b<sub>1</sub></span>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;⇒&nbsp;<span class="id" type="var">negb</span>&nbsp;(<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">b<sub>1</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">BAnd</span>&nbsp;<span class="id" type="var">b<sub>1</sub></span>&nbsp;<span class="id" type="var">b<sub>2</sub></span>&nbsp;&nbsp;⇒&nbsp;<span class="id" type="var">andb</span>&nbsp;(<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">b<sub>1</sub></span>)&nbsp;(<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">b<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span>.
<div class="paragraph"> </div>

</div>
    请用推理规则记法将布尔求值的定义写成关系的形式。 
</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_beval_rules</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab338"></a><h2 class="section">定义的等价关系</h2>

<div class="paragraph"> </div>

 求值的函数式定义与关系式定义之间的一致性证明非常直观： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">aeval_iff_aevalR</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span> <span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;(<span class="id" type="var">a</span> \\ <span class="id" type="var">n</span>) ↔ <span class="id" type="var">aeval</span> <span class="id" type="var">a</span> = <span class="id" type="var">n</span>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_ANum&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_APlus&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHaevalR1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHaevalR2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_AMinus&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHaevalR1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHaevalR2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_AMult&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHaevalR1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHaevalR2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">n</span>.<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;ANum&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_ANum</span>.<br/>
&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;APlus&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_APlus</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;AMinus&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_AMinus</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;AMult&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_AMult</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHa1</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHa2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
我们可以利用泛策略将此证明缩减到很短。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">aeval_iff_aevalR'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span> <span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;(<span class="id" type="var">a</span> \\ <span class="id" type="var">n</span>) ↔ <span class="id" type="var">aeval</span> <span class="id" type="var">a</span> = <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;课上已完成&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">n</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>; <span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="var">constructor</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab339"></a><h4 class="section">练习：3 星, standard (bevalR)</h4>
 用和 <span class="inlinecode"><span class="id" type="var">aevalR</span></span> 同样的方式写出关系 <span class="inlinecode"><span class="id" type="var">bevalR</span></span>，并证明它等价于 <span class="inlinecode"><span class="id" type="var">beval</span></span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">bevalR</span>: <span class="id" type="var">bexp</span> → <span class="id" type="var">bool</span> → <span class="id" type="keyword">Prop</span> :=<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">beval_iff_bevalR</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">bv</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bevalR</span> <span class="id" type="var">b</span> <span class="id" type="var">bv</span> ↔ <span class="id" type="var">beval</span> <span class="id" type="var">b</span> = <span class="id" type="var">bv</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">AExp</span>.<br/>
</div>

<div class="doc">
<a name="lab340"></a><h2 class="section">计算式定义与关系式定义</h2>

<div class="paragraph"> </div>

 对于算术和布尔表达式求值的定义方式而言，函数式和关系式二者均可，
    选择哪种主要取决于品味。

<div class="paragraph"> </div>

    然而在某些情况下，求值的关系式定义比函数式定义要更好。  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">aevalR_division</span>.<br/>
</div>

<div class="doc">
例如，假设我们想要用除法来扩展算术运算： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">aexp</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">ANum</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMinus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMult</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ADiv</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>). <span class="comment">(*&nbsp;&lt;---&nbsp;新增&nbsp;*)</span><br/>
</div>

<div class="doc">
扩展 <span class="inlinecode"><span class="id" type="var">aeval</span></span> 的定义来处理此讯算并不是很直观（我们要返回什么作为
    <span class="inlinecode"><span class="id" type="var">ADiv</span></span> <span class="inlinecode">(<span class="id" type="var">ANum</span></span> <span class="inlinecode">5)</span> <span class="inlinecode">(<span class="id" type="var">ANum</span></span> <span class="inlinecode">0)</span> 的结果？）。然而扩展 <span class="inlinecode"><span class="id" type="var">aevalR</span></span> 却很直观。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Reserved Notation</span> "e '\\' n"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 90, <span class="id" type="var">left</span> <span class="id" type="var">associativity</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">aevalR</span> : <span class="id" type="var">aexp</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_ANum</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">ANum</span> <span class="id" type="var">n</span>) \\ <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_APlus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">a<sub>1</sub></span> \\ <span class="id" type="var">n<sub>1</sub></span>) → (<span class="id" type="var">a<sub>2</sub></span> \\ <span class="id" type="var">n<sub>2</sub></span>) → (<span class="id" type="var">APlus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>) \\ (<span class="id" type="var">n<sub>1</sub></span> + <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_AMinus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">a<sub>1</sub></span> \\ <span class="id" type="var">n<sub>1</sub></span>) → (<span class="id" type="var">a<sub>2</sub></span> \\ <span class="id" type="var">n<sub>2</sub></span>) → (<span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>) \\ (<span class="id" type="var">n<sub>1</sub></span> - <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_AMult</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">a<sub>1</sub></span> \\ <span class="id" type="var">n<sub>1</sub></span>) → (<span class="id" type="var">a<sub>2</sub></span> \\ <span class="id" type="var">n<sub>2</sub></span>) → (<span class="id" type="var">AMult</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>) \\ (<span class="id" type="var">n<sub>1</sub></span> * <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_ADiv</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> <span class="id" type="var">n<sub>3</sub></span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">a<sub>1</sub></span> \\ <span class="id" type="var">n<sub>1</sub></span>) → (<span class="id" type="var">a<sub>2</sub></span> \\ <span class="id" type="var">n<sub>2</sub></span>) → (<span class="id" type="var">n<sub>2</sub></span> &gt; 0) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">mult</span> <span class="id" type="var">n<sub>2</sub></span> <span class="id" type="var">n<sub>3</sub></span> = <span class="id" type="var">n<sub>1</sub></span>) → (<span class="id" type="var">ADiv</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>) \\ <span class="id" type="var">n<sub>3</sub></span><br/>
<br/>
<span class="id" type="keyword">where</span> "a '\\' n" := (<span class="id" type="var">aevalR</span> <span class="id" type="var">a</span> <span class="id" type="var">n</span>) : <span class="id" type="var">type_scope</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">aevalR_division</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">aevalR_extended</span>.<br/>
</div>

<div class="doc">
假设我们想要用非确定性的数值生成器 <span class="inlinecode"><span class="id" type="var">any</span></span> 来扩展算术运算，
    该生成器会在求值时产生任何数。（注意，这不同于在所有可能的数值中作出
    <b>概率上的</b>选择 &mdash; 我们没有为结果指定任何具体的概率分布，只是说了
    <b>可能的结果</b>。） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Reserved Notation</span> "e '\\' n" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 90, <span class="id" type="var">left</span> <span class="id" type="var">associativity</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">aexp</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">AAny</span>                           <span class="comment">(*&nbsp;&lt;---&nbsp;NEW&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ANum</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMinus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMult</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>).<br/>
</div>

<div class="doc">
同样，扩展 <span class="inlinecode"><span class="id" type="var">aeval</span></span> 会很棘手，因为现在的求值<b>并不是</b>一个从表达式到数值的确定性函数，
    而扩展 <span class="inlinecode"><span class="id" type="var">aevalR</span></span> 则无此问题... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">aevalR</span> : <span class="id" type="var">aexp</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_Any</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">AAny</span> \\ <span class="id" type="var">n</span>                        <span class="comment">(*&nbsp;&lt;---&nbsp;NEW&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_ANum</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">ANum</span> <span class="id" type="var">n</span>) \\ <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_APlus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">a<sub>1</sub></span> \\ <span class="id" type="var">n<sub>1</sub></span>) → (<span class="id" type="var">a<sub>2</sub></span> \\ <span class="id" type="var">n<sub>2</sub></span>) → (<span class="id" type="var">APlus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>) \\ (<span class="id" type="var">n<sub>1</sub></span> + <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_AMinus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">a<sub>1</sub></span> \\ <span class="id" type="var">n<sub>1</sub></span>) → (<span class="id" type="var">a<sub>2</sub></span> \\ <span class="id" type="var">n<sub>2</sub></span>) → (<span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>) \\ (<span class="id" type="var">n<sub>1</sub></span> - <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_AMult</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> : <span class="id" type="var">nat</span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">a<sub>1</sub></span> \\ <span class="id" type="var">n<sub>1</sub></span>) → (<span class="id" type="var">a<sub>2</sub></span> \\ <span class="id" type="var">n<sub>2</sub></span>) → (<span class="id" type="var">AMult</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>) \\ (<span class="id" type="var">n<sub>1</sub></span> * <span class="id" type="var">n<sub>2</sub></span>)<br/>
<br/>
<span class="id" type="keyword">where</span> "a '\\' n" := (<span class="id" type="var">aevalR</span> <span class="id" type="var">a</span> <span class="id" type="var">n</span>) : <span class="id" type="var">type_scope</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">aevalR_extended</span>.<br/>
</div>

<div class="doc">
这时你可能会问：默认情况下应该使用哪种风格？
    我们刚看到的例子表明关系式的定义反而比函数式的更加有用。
    对于这种定义的东西不太容易用函数表达，或者确实<b>不是</b>函数的情况来说，
    明显别无选择。但如果两种风格均可行呢？

<div class="paragraph"> </div>

    关系式定义的一个优点是，它们会更优雅，更容易理解。

<div class="paragraph"> </div>

    另一个优点是，Coq 会根据 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 定义自动生成不错的反演函数和归纳法则。 
<div class="paragraph"> </div>

 另一方面，函数式定义通常会更方便：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 函数的定义是确定性的，且在所有参数上定义；而对于关系式定义来说，
       我们需要这些性质时必须显式地证明它们。

</li>
<li> 有了函数，我们还可以利用 Coq 的计算机制在证明过程中简化表达式。

</li>
</ul>

<div class="paragraph"> </div>

    此外，函数还可以直接从 Gallina“提取”出 OCaml 或 Haskell 的可执行代码。 
<div class="paragraph"> </div>

 最终，选择视具体情况而定，或者只是品味问题。确实，在大型的 Coq
    开发中，经常可以看到一个定义同时给出了函数式和关系式<b>两种</b>风格，
    加上一条陈述了二者等价的引理，以便在之后的证明中能够在这两种视角下随意切换。 
</div>

<div class="doc">
<a name="lab341"></a><h1 class="section">带变量的表达式</h1>

<div class="paragraph"> </div>

 让我们回到 Imp 的定义上来。接下来我们要为算术和布尔表达式加上变量。
    为简单起见，我们会假设所有变量是都全局的，且它们只保存数值。 
</div>

<div class="doc">
<a name="lab342"></a><h2 class="section">状态</h2>

<div class="paragraph"> </div>

 由于需要查找变量来获得它们的具体值，因此我们重用了 <a href="Maps.html"><span class="inlineref">Maps</span></a>
    一章中的映射。我们在 Imp 中以 <span class="inlinecode"><span class="id" type="var">string</span></span> 作为变量的类型。

<div class="paragraph"> </div>

    <b>机器的状态</b>（简称<b>状态</b>）表示程序执行中某一时刻<b>所有变量</b>的值。 
<div class="paragraph"> </div>

 虽然任何给定的程序只会涉及有限数量的变量，不过为简单起见，
    我们假设状态为<b>所有的</b>变量定义。状态会捕获内存中所有的信息。
    对 Imp 程序而言，由于每个变量都存储了一个自然数，
    因此我们可以将状态表示为一个从字符串到 <span class="inlinecode"><span class="id" type="var">nat</span></span> 的映射，并且用 <span class="inlinecode">0</span>
    作为存储中的默认值。对于更复杂的编程语言，状态会有更多结构。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">state</span> := <span class="id" type="var">total_map</span> <span class="id" type="var">nat</span>.<br/>
</div>

<div class="doc">
<a name="lab343"></a><h2 class="section">语法</h2>

<div class="paragraph"> </div>

 我们只需为之前的算术表达式再加一个构造子就能添加变量： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">aexp</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">ANum</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AId</span> (<span class="id" type="var">x</span> :  <span class="id" type="var">string</span>)             <span class="comment">(*&nbsp;&lt;---&nbsp;新增&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMinus</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMult</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>).<br/>
</div>

<div class="doc">
为几个变量名定义简单记法能让示例更加易读： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">W</span> : <span class="id" type="var">string</span> := "W".<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">X</span> : <span class="id" type="var">string</span> := "X".<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">Y</span> : <span class="id" type="var">string</span> := "Y".<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">Z</span> : <span class="id" type="var">string</span> := "Z".<br/>
</div>

<div class="doc">
（这种命名程序变量的约定（<span class="inlinecode"><span class="id" type="var">X</span></span>、<span class="inlinecode"><span class="id" type="var">Y</span></span>、<span class="inlinecode"><span class="id" type="var">Z</span></span>）
    与我们之前使用大写字母表示类型有点冲突。由于我们在本章中开发 Imp
    时没怎么使用多态，所以这种重载应该不会产生混淆。） 
<div class="paragraph"> </div>

 <span class="inlinecode"><span class="id" type="var">bexp</span></span> 的定义现在除了引用了新的 <span class="inlinecode"><span class="id" type="var">aexp</span></span> 之外并未更改： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">bexp</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">BTrue</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BEq</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BLe</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BNot</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BAnd</span> (<span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> : <span class="id" type="var">bexp</span>).<br/>
</div>

<div class="doc">
<a name="lab344"></a><h2 class="section">记法</h2>
 要让 Imp 程序更易读写，我们引入了一些记法和隐式转换（Coercion）。

<div class="paragraph"> </div>

    你无需理解以下声明具体做了些什么。简言而之，Coq 中的 <span class="inlinecode"><span class="id" type="keyword">Coercion</span></span>
    声明规定了一个函数（或构造子）可以被类型系统隐式地用于将一个输入类型的值
    转换成输出类型的值。例如，<span class="inlinecode"><span class="id" type="var">AId</span></span> 的转换声明在需要一个 <span class="inlinecode"><span class="id" type="var">aexp</span></span>
    时直接使用普通的字符串，该字符串会被隐式地用 <span class="inlinecode"><span class="id" type="var">AId</span></span> 来包装。 
<div class="paragraph"> </div>

 下列记法在具体的<b>记法作用域</b>中声明，以避免与其它符号相同的解释相冲突。
    同样，你暂时也无需理解其中的细节，但要意识到到我们为 <span class="inlinecode">+</span>、<span class="inlinecode">-</span>、<span class="inlinecode">*</span>、<span class="inlinecode">=</span>、<span class="inlinecode">≤</span>
    等运算符定义了<b>新的</b>解释十分重要。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Coercion</span> <span class="id" type="var">AId</span> : <span class="id" type="var">string</span> &gt;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">aexp</span>.<br/>
<span class="id" type="keyword">Coercion</span> <span class="id" type="var">ANum</span> : <span class="id" type="var">nat</span> &gt;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">aexp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">bool_to_bexp</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bool</span>) : <span class="id" type="var">bexp</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">b</span> <span class="id" type="keyword">then</span> <span class="id" type="var">BTrue</span> <span class="id" type="keyword">else</span> <span class="id" type="var">BFalse</span>.<br/>
<span class="id" type="keyword">Coercion</span> <span class="id" type="var">bool_to_bexp</span> : <span class="id" type="var">bool</span> &gt;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">bexp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Bind</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span> <span class="id" type="keyword">with</span> <span class="id" type="var">aexp</span>.<br/>
<span class="id" type="keyword">Bind</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span> <span class="id" type="keyword">with</span> <span class="id" type="var">bexp</span>.<br/>
<span class="id" type="keyword">Delimit</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span> <span class="id" type="keyword">with</span> <span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> "x + y" := (<span class="id" type="var">APlus</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 50, <span class="id" type="var">left</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "x - y" := (<span class="id" type="var">AMinus</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 50, <span class="id" type="var">left</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "x * y" := (<span class="id" type="var">AMult</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40, <span class="id" type="var">left</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "x ≤ y" := (<span class="id" type="var">BLe</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 70, <span class="id" type="var">no</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "x = y" := (<span class="id" type="var">BEq</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 70, <span class="id" type="var">no</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "x &amp;&amp; y" := (<span class="id" type="var">BAnd</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40, <span class="id" type="var">left</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "'¬' b" := (<span class="id" type="var">BNot</span> <span class="id" type="var">b</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 75, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
</div>

<div class="doc">
现在我们可以用 <span class="inlinecode">3</span> <span class="inlinecode">+</span> <span class="inlinecode">(<span class="id" type="var">X</span></span> <span class="inlinecode">*</span> <span class="inlinecode">2)</span> 来代替 <span class="inlinecode"><span class="id" type="var">APlus</span></span> <span class="inlinecode">3</span> <span class="inlinecode">(<span class="id" type="var">AMult</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">2)</span> 了，同样可以用
    <span class="inlinecode"><span class="id" type="var">true</span></span> <span class="inlinecode">&amp;&amp;</span> <span class="inlinecode">!(<span class="id" type="var">X</span></span> <span class="inlinecode">≤</span> <span class="inlinecode">4)</span> 来代替 <span class="inlinecode"><span class="id" type="var">BAnd</span></span> <span class="inlinecode"><span class="id" type="var">true</span></span> <span class="inlinecode">(<span class="id" type="var">BNot</span></span> <span class="inlinecode">(<span class="id" type="var">BLe</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">4))</span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">example_aexp</span> := (3 + (<span class="id" type="var">X</span> * 2))%<span class="id" type="var">imp</span> : <span class="id" type="var">aexp</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">example_bexp</span> := (<span class="id" type="var">true</span> &amp;&amp; ~(<span class="id" type="var">X</span> ≤ 4))%<span class="id" type="var">imp</span> : <span class="id" type="var">bexp</span>.<br/>
</div>

<div class="doc">
强制转换有一点不便之处，即它会略微提高人类推导表达式类型的难度。
    如果你感到有点困惑，请用 <span class="inlinecode"><span class="id" type="keyword">Set</span></span> <span class="inlinecode"><span class="id" type="var">Printing</span></span> <span class="inlinecode"><span class="id" type="var">Coercions</span></span> 来查看具体发生了什么。 
</div>
<div class="code code-tight">

<span class="id" type="var">Set Printing Coercions</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Print</span> <span class="id" type="var">example_bexp</span>.<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;example_bexp&nbsp;=&nbsp;bool_to_bexp&nbsp;true&nbsp;&amp;&amp;&nbsp;~&nbsp;(AId&nbsp;X&nbsp;&lt;=&nbsp;ANum&nbsp;4)&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="var">Unset Printing Coercions</span>.<br/>
</div>

<div class="doc">
<a name="lab345"></a><h2 class="section">求值</h2>

<div class="paragraph"> </div>

 算术和布尔求值器被扩展成以很显然的方式来处理变量，
    它接受一个状态作为额外的参数： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">aeval</span> (<span class="id" type="var">st</span> : <span class="id" type="var">state</span>) (<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>) : <span class="id" type="var">nat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">a</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ANum</span> <span class="id" type="var">n</span> ⇒ <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">AId</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="var">st</span> <span class="id" type="var">x</span>                                <span class="comment">(*&nbsp;&lt;---&nbsp;新增&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span>) + (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span>) - (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMult</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span>) * (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">beval</span> (<span class="id" type="var">st</span> : <span class="id" type="var">state</span>) (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) : <span class="id" type="var">bool</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">b</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BTrue</span>       ⇒ <span class="id" type="var">true</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BFalse</span>      ⇒ <span class="id" type="var">false</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BEq</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>   ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span>) =? (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BLe</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>   ⇒ (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span>) &lt;=? (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BNot</span> <span class="id" type="var">b<sub>1</sub></span>     ⇒ <span class="id" type="var">negb</span> (<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b<sub>1</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">BAnd</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span>  ⇒ <span class="id" type="var">andb</span> (<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b<sub>1</sub></span>) (<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b<sub>2</sub></span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
我们为具体状态的全映射声明具体的记法，即使用 <span class="inlinecode">(<span class="id" type="var">_</span></span> <span class="inlinecode">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">0)</span> 作为空状态。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">empty_st</span> := (<span class="id" type="var">_</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 0).<br/>
</div>

<div class="doc">
现在我们可以为“单例状态（singleton state）”添加新的记法了，
    即只有一个绑定到值的变量。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Notation</span> "a '!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>' x" := (<span class="id" type="var">t_update</span> <span class="id" type="var">empty_st</span> <span class="id" type="var">a</span> <span class="id" type="var">x</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 100).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">aexp1</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aeval</span> (<span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 5) (3 + (<span class="id" type="var">X</span> * 2))%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;= 13.<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">bexp1</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> (<span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 5) (<span class="id" type="var">true</span> &amp;&amp; ~(<span class="id" type="var">X</span> ≤ 4))%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;= <span class="id" type="var">true</span>.<br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab346"></a><h1 class="section">指令</h1>

<div class="paragraph"> </div>

 现在我们可以定义 Imp <b>指令（Command）</b>（有时称作<b>语句（Statement）</b>）
    的语法和行为了。 
</div>

<div class="doc">
<a name="lab347"></a><h2 class="section">语法</h2>

<div class="paragraph"> </div>

 指令 <span class="inlinecode"><span class="id" type="var">c</span></span> 可以用以下 BNF 文法非形式化地描述。

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">SKIP</span>&nbsp;|&nbsp;<span class="id" type="var">x</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a</span>&nbsp;|&nbsp;<span class="id" type="var">c</span>&nbsp;;;&nbsp;<span class="id" type="var">c</span>&nbsp;|&nbsp;<span class="id" type="var">TEST</span>&nbsp;<span class="id" type="var">b</span>&nbsp;<span class="id" type="var">THEN</span>&nbsp;<span class="id" type="var">c</span>&nbsp;<span class="id" type="var">ELSE</span>&nbsp;<span class="id" type="var">c</span>&nbsp;<span class="id" type="var">FI</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">WHILE</span>&nbsp;<span class="id" type="var">b</span>&nbsp;<span class="id" type="var">DO</span>&nbsp;<span class="id" type="var">c</span>&nbsp;<span class="id" type="var">END</span>
<div class="paragraph"> </div>

</div>
    （为了能够使用 Coq 的记法机制来定义 Imp 语法，我们选择了这种略尴尬的具体语法。
    具体来说，我们使用了 <span class="inlinecode"><span class="id" type="var">TEST</span></span> 来避免与表中库中的 <span class="inlinecode"><span class="id" type="keyword">if</span></span> 记法相冲突。） 
<div class="paragraph"> </div>

    例如，下面是用 Imp 编写的阶乘：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Z</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">WHILE</span>&nbsp;~(<span class="id" type="var">Z</span>&nbsp;=&nbsp;0)&nbsp;<span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;*&nbsp;<span class="id" type="var">Z</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Z</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">Z</span>&nbsp;-&nbsp;1<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>
<div class="paragraph"> </div>

</div>
   当此指令终止后，<span class="inlinecode"><span class="id" type="var">Y</span></span> 会保存初始值 <span class="inlinecode"><span class="id" type="var">X</span></span> 的阶乘。 
<div class="paragraph"> </div>

 下面是指令的抽象语法的形式化定义： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">com</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">CSkip</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CAss</span> (<span class="id" type="var">x</span> : <span class="id" type="var">string</span>) (<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">CSeq</span> (<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">CIf</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) (<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">CWhile</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) (<span class="id" type="var">c</span> : <span class="id" type="var">com</span>).<br/>
</div>

<div class="doc">
至于表达式，我们可以用一些 <span class="inlinecode"><span class="id" type="keyword">Notation</span></span> 声明来让 Imp 程序的读写更加方便。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Bind</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span> <span class="id" type="keyword">with</span> <span class="id" type="var">com</span>.<br/>
<span class="id" type="keyword">Notation</span> "'SKIP'" :=<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">CSkip</span> : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "x '<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>' a" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CAss</span> <span class="id" type="var">x</span> <span class="id" type="var">a</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 60) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "c<sub>1</sub> ;; c<sub>2</sub>" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CSeq</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "'WHILE' b 'DO' c 'END'" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CWhile</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "'TEST' c<sub>1</sub> 'THEN' c<sub>2</sub> 'ELSE' c<sub>3</sub> 'FI'" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CIf</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>3</sub></span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
</div>

<div class="doc">
例如，下面是个阶乘函数，写成 Coq 的形式化定义： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">fact_in_coq</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">Z</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span>;;<br/>
&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 1;;<br/>
&nbsp;&nbsp;<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">Z</span> = 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">Y</span> * <span class="id" type="var">Z</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Z</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">Z</span> - 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/>
</div>

<div class="doc">
<a name="lab348"></a><h2 class="section">脱糖记法</h2>

<div class="paragraph"> </div>

 Coq 为管理日益复杂的工作对象提供了丰富的特性，例如隐式转换和记法。
    然而，过度使用它们会产生繁杂的语法。为了教学，我们通常会用以下命令来
    “关闭”这些特性以获得对事物更加本质的描述：

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="keyword">Unset</span></span> <span class="inlinecode"><span class="id" type="var">Printing</span></span> <span class="inlinecode"><span class="id" type="var">Notations</span></span>（用 <span class="inlinecode"><span class="id" type="keyword">Set</span></span> <span class="inlinecode"><span class="id" type="var">Printing</span></span> <span class="inlinecode"><span class="id" type="var">Notations</span></span> 撤销）

</li>
<li> <span class="inlinecode"><span class="id" type="keyword">Set</span></span> <span class="inlinecode"><span class="id" type="var">Printing</span></span> <span class="inlinecode"><span class="id" type="var">Coercions</span></span>（用 <span class="inlinecode"><span class="id" type="keyword">Unset</span></span> <span class="inlinecode"><span class="id" type="var">Printing</span></span> <span class="inlinecode"><span class="id" type="var">Coercions</span></span> 撤销）

</li>
<li> <span class="inlinecode"><span class="id" type="keyword">Set</span></span> <span class="inlinecode"><span class="id" type="var">Printing</span></span> <span class="inlinecode"><span class="id" type="var">All</span></span>（用 <span class="inlinecode"><span class="id" type="keyword">Unset</span></span> <span class="inlinecode"><span class="id" type="var">Printing</span></span> <span class="inlinecode"><span class="id" type="var">All</span></span> 撤销）

</li>
</ul>
    这些命令也可在证明过程中详述当前目标和上下文。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Unset</span> <span class="id" type="var">Printing</span> <span class="id" type="var">Notations</span>.<br/>
<span class="id" type="keyword">Print</span> <span class="id" type="var">fact_in_coq</span>.<br/>
<span class="comment">(*&nbsp;===&gt;<br/>
&nbsp;&nbsp;&nbsp;fact_in_coq&nbsp;=<br/>
&nbsp;&nbsp;&nbsp;CSeq&nbsp;(CAss&nbsp;Z&nbsp;X)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(CSeq&nbsp;(CAss&nbsp;Y&nbsp;(S&nbsp;O))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(CWhile&nbsp;(BNot&nbsp;(BEq&nbsp;Z&nbsp;O))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(CSeq&nbsp;(CAss&nbsp;Y&nbsp;(AMult&nbsp;Y&nbsp;Z))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(CAss&nbsp;Z&nbsp;(AMinus&nbsp;Z&nbsp;(S&nbsp;O))))))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:&nbsp;com&nbsp;*)</span><br/>
<span class="id" type="keyword">Set</span> <span class="id" type="var">Printing</span> <span class="id" type="var">Notations</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">Set Printing Coercions</span>.<br/>
<span class="id" type="keyword">Print</span> <span class="id" type="var">fact_in_coq</span>.<br/>
<span class="comment">(*&nbsp;===&gt;<br/>
&nbsp;&nbsp;&nbsp;fact_in_coq&nbsp;=<br/>
&nbsp;&nbsp;&nbsp;(Z&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;AId&nbsp;X;;<br/>
&nbsp;&nbsp;&nbsp;Y&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;ANum&nbsp;1;;<br/>
&nbsp;&nbsp;&nbsp;WHILE&nbsp;~&nbsp;(AId&nbsp;Z&nbsp;=&nbsp;ANum&nbsp;0)&nbsp;DO<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Y&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;AId&nbsp;Y&nbsp;*&nbsp;AId&nbsp;Z;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Z&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;AId&nbsp;Z&nbsp;-&nbsp;ANum&nbsp;1<br/>
&nbsp;&nbsp;&nbsp;END)%imp<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:&nbsp;com&nbsp;*)</span><br/>
<span class="id" type="var">Unset Printing Coercions</span>.<br/>
</div>

<div class="doc">
<a name="lab349"></a><h2 class="section"><span class="inlinecode"><span class="id" type="var">Locate</span></span> 命令</h2>

<div class="paragraph"> </div>

<a name="lab350"></a><h3 class="section">查询记法</h3>

<div class="paragraph"> </div>

 当遇到未知记法时，可使用 <span class="inlinecode"><span class="id" type="var">Locate</span></span> 后跟一个包含其符号的<b>字符串</b>
    来查看其可能的解释。 
</div>
<div class="code code-tight">
<span class="id" type="var">Locate</span> "&amp;&amp;".<br/>
<span class="comment">(*&nbsp;===&gt;<br/>
&nbsp;&nbsp;&nbsp;Notation&nbsp;"x&nbsp;&amp;&amp;&nbsp;y"&nbsp;:=&nbsp;andb&nbsp;x&nbsp;y&nbsp;:&nbsp;bool_scope&nbsp;(default&nbsp;interpretation)&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="var">Locate</span> ";;".<br/>
<span class="comment">(*&nbsp;===&gt;<br/>
&nbsp;&nbsp;&nbsp;Notation&nbsp;"c<sub>1</sub>&nbsp;;;&nbsp;c<sub>2</sub>"&nbsp;:=&nbsp;CSeq&nbsp;c<sub>1</sub>&nbsp;c<sub>2</sub>&nbsp;:&nbsp;imp_scope&nbsp;(default&nbsp;interpretation)&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="var">Locate</span> "WHILE".<br/>
<span class="comment">(*&nbsp;===&gt;<br/>
&nbsp;&nbsp;&nbsp;Notation&nbsp;"'WHILE'&nbsp;b&nbsp;'DO'&nbsp;c&nbsp;'END'"&nbsp;:=&nbsp;CWhile&nbsp;b&nbsp;c&nbsp;:&nbsp;imp_scope<br/>
&nbsp;&nbsp;&nbsp;(default&nbsp;interpretation)&nbsp;*)</span><br/>
</div>

<div class="doc">
<a name="lab351"></a><h3 class="section">查询标识符</h3>

<div class="paragraph"> </div>

 当以标示符使用 <span class="inlinecode"><span class="id" type="var">Locate</span></span> 时，它会打印作用域中同名的所有值的完成路径。
    它很适合解决由变量覆盖所引起的问题。 
</div>
<div class="code code-tight">
<span class="id" type="var">Locate</span> <span class="id" type="var">aexp</span>.<br/>
<span class="comment">(*&nbsp;===&gt;<br/>
&nbsp;&nbsp;&nbsp;Inductive&nbsp;Top.aexp<br/>
&nbsp;&nbsp;&nbsp;Inductive&nbsp;Top.AExp.aexp<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(shorter&nbsp;name&nbsp;to&nbsp;refer&nbsp;to&nbsp;it&nbsp;in&nbsp;current&nbsp;context&nbsp;is&nbsp;AExp.aexp)<br/>
&nbsp;&nbsp;&nbsp;Inductive&nbsp;Top.aevalR_division.aexp<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(shorter&nbsp;name&nbsp;to&nbsp;refer&nbsp;to&nbsp;it&nbsp;in&nbsp;current&nbsp;context&nbsp;is&nbsp;aevalR_division.aexp)<br/>
&nbsp;&nbsp;&nbsp;Inductive&nbsp;Top.aevalR_extended.aexp<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(shorter&nbsp;name&nbsp;to&nbsp;refer&nbsp;to&nbsp;it&nbsp;in&nbsp;current&nbsp;context&nbsp;is&nbsp;aevalR_extended.aexp)<br/>
*)</span><br/>
</div>

<div class="doc">
<a name="lab352"></a><h2 class="section">更多示例</h2>

<div class="paragraph"> </div>

 赋值： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">plus2</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 2.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">XtimesYinZ</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">Z</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> * <span class="id" type="var">Y</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">subtract_slowly_body</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">Z</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">Z</span> - 1 ;;<br/>
&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> - 1.<br/>
</div>

<div class="doc">
<a name="lab353"></a><h3 class="section">循环</h3>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">subtract_slowly</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">subtract_slowly_body</span><br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">subtract_3_from_5_slowly</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 3 ;;<br/>
&nbsp;&nbsp;<span class="id" type="var">Z</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 5 ;;<br/>
&nbsp;&nbsp;<span class="id" type="var">subtract_slowly</span>.<br/>
</div>

<div class="doc">
<a name="lab354"></a><h3 class="section">无限循环：</h3>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">loop</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">WHILE</span> <span class="id" type="var">true</span> <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>.<br/>
</div>

<div class="doc">
<a name="lab355"></a><h1 class="section">求值指令</h1>

<div class="paragraph"> </div>

 接下来我们要定义对 Imp 指令进行求值是什么意思。
    <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 未必会终止的事实让定义它的求值函数有点棘手... 
</div>

<div class="doc">
<a name="lab356"></a><h2 class="section">求值作为函数（失败的尝试）</h2>

<div class="paragraph"> </div>

 下面是一次为指令定义求值函数的尝试，我们忽略了 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 的情况。 
<div class="paragraph"> </div>

 为了在模式匹配中使用记法，我们需要以下声明。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">ceval_fun_no_while</span> (<span class="id" type="var">st</span> : <span class="id" type="var">state</span>) (<span class="id" type="var">c</span> : <span class="id" type="var">com</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">state</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">c</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">SKIP</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span>) ; <span class="id" type="var">st</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">c<sub>1</sub></span> ;; <span class="id" type="var">c<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">let</span> <span class="id" type="var">st'</span> := <span class="id" type="var">ceval_fun_no_while</span> <span class="id" type="var">st</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="keyword">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ceval_fun_no_while</span> <span class="id" type="var">st'</span> <span class="id" type="var">c<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">if</span> (<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">then</span> <span class="id" type="var">ceval_fun_no_while</span> <span class="id" type="var">st</span> <span class="id" type="var">c<sub>1</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span> <span class="id" type="var">ceval_fun_no_while</span> <span class="id" type="var">st</span> <span class="id" type="var">c<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  <span class="comment">(*&nbsp;假装能用&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
<span class="id" type="var">Close</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span>.<br/>
</div>

<div class="doc">
在 OCaml 或 Haskell 这类传统的函数式编程语言中，我们可以像下面这样添加
    <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 的情况：
<pre>
        Fixpoint ceval_fun (st : state) (c : com) : state :=
          match c with
            ...
            | WHILE b DO c END =&gt;
                if (beval st b)
                  then ceval_fun st (c ;; WHILE b DO c END)
                  else st
          end.
</pre>
    Coq 会拒绝这种定义（“Error: Cannot guess decreasing argument of fix”，
    错误：无法猜测出固定的递减参数），因为我们想要定义的函数并不保证终止。
    确实，它并不<b>总是会终止</b>：例如，<span class="inlinecode"><span class="id" type="var">ceval_fun</span></span> 函数应用到上面的 <span class="inlinecode"><span class="id" type="var">loop</span></span>
    程序的完整版本永远不会终止。由于 Coq 不仅是一个函数式编程语言，
    还是个逻辑一致的语言，因此任何潜在的不可终止函数都会被拒绝。下面是一个
    （无效的）程序，它展示了如果 Coq 允许不可终止的递归函数的话会产生什么错误：
<pre>
         Fixpoint loop_false (n : nat) : False := loop_false n.
</pre>
    也就是说，像 <span class="inlinecode"><span class="id" type="var">False</span></span> 这样的假命题可以被证明（<span class="inlinecode"><span class="id" type="var">loop_false</span></span> <span class="inlinecode">0</span> 会是 <span class="inlinecode"><span class="id" type="var">False</span></span>
    的一个证明），这对于 Coq 的逻辑一致性来说是个灾难。

<div class="paragraph"> </div>

    由于它对于所有的输入都不会终止，因此 <span class="inlinecode"><span class="id" type="var">ceval_fun</span></span> 无法在 Coq 中写出
 至少需要一些技巧和变通才行（如果你对此好奇的话请阅读
    <a href="ImpCEvalFun.html"><span class="inlineref">ImpCEvalFun</span></a> 一章）。 
</div>

<div class="doc">
<a name="lab357"></a><h2 class="section">求值作为一种关系</h2>

<div class="paragraph"> </div>

 下面是一种更好的方法：将 <span class="inlinecode"><span class="id" type="var">ceval</span></span> 定义成一种<b>关系</b>而非一个<b>函数</b>
 即，用 <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> 而非用 <span class="inlinecode"><span class="id" type="keyword">Type</span></span> 来定义它，和我们前面对 <span class="inlinecode"><span class="id" type="var">aevalR</span></span> 做的那样。 
<div class="paragraph"> </div>

 这是一个非常重要的更改。除了能将我们从尴尬的变通中解放出来之外，
    它还给我们的定义赋予了更多的灵活性。例如，如果我们要为该语言添加更多像
    <span class="inlinecode"><span class="id" type="var">any</span></span> 这样非确定性的特性，我们需要让求值的定义也是非确定性的 &mdash;
    即，它不仅会有不完全性，甚至还可以不是个函数！ 
<div class="paragraph"> </div>

 我们将使用记法 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 来表示 <span class="inlinecode"><span class="id" type="var">ceval</span></span> 这种关系：<span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>
    表示在开始状态 <span class="inlinecode"><span class="id" type="var">st</span></span> 下启动程序并在结束状态 <span class="inlinecode"><span class="id" type="var">st'</span></span> 下产生结果。它可以读作：
    “<span class="inlinecode"><span class="id" type="var">c</span></span> 将状态 <span class="inlinecode"><span class="id" type="var">st</span></span> 变成 <span class="inlinecode"><span class="id" type="var">st'</span></span>”。 
<div class="paragraph"> </div>

<a name="lab358"></a><h3 class="section">操作语义</h3>

<div class="paragraph"> </div>

 下面是求值的非形式化定义，为了可读性表示成推理规则：
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (E_Skip) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">st&nbsp;=[&nbsp;SKIP&nbsp;]=>&nbsp;st</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">aeval&nbsp;st&nbsp;a<sub>1</sub>&nbsp;=&nbsp;n</td>
  <td class="infrulenamecol" rowspan="3">
    (E_Ass) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">st&nbsp;=[&nbsp;x&nbsp;:=&nbsp;a<sub>1</sub>&nbsp;]=>&nbsp;(x&nbsp;!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;n&nbsp;;&nbsp;st)</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">st&nbsp;&nbsp;=[&nbsp;c<sub>1</sub>&nbsp;]=>&nbsp;st'</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">st'&nbsp;=[&nbsp;c<sub>2</sub>&nbsp;]=>&nbsp;st''</td>
  <td class="infrulenamecol" rowspan="3">
    (E_Seq) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">st&nbsp;=[&nbsp;c<sub>1</sub>;;c<sub>2</sub>&nbsp;]=>&nbsp;st''</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">beval&nbsp;st&nbsp;b<sub>1</sub>&nbsp;=&nbsp;true</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">st&nbsp;=[&nbsp;c<sub>1</sub>&nbsp;]=>&nbsp;st'</td>
  <td class="infrulenamecol" rowspan="3">
    (E_IfTrue) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">st&nbsp;=[&nbsp;TEST&nbsp;b<sub>1</sub>&nbsp;THEN&nbsp;c<sub>1</sub>&nbsp;ELSE&nbsp;c<sub>2</sub>&nbsp;FI&nbsp;]=>&nbsp;st'</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">beval&nbsp;st&nbsp;b<sub>1</sub>&nbsp;=&nbsp;false</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">st&nbsp;=[&nbsp;c<sub>2</sub>&nbsp;]=>&nbsp;st'</td>
  <td class="infrulenamecol" rowspan="3">
    (E_IfFalse) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">st&nbsp;=[&nbsp;TEST&nbsp;b<sub>1</sub>&nbsp;THEN&nbsp;c<sub>1</sub>&nbsp;ELSE&nbsp;c<sub>2</sub>&nbsp;FI&nbsp;]=>&nbsp;st'</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">beval&nbsp;st&nbsp;b&nbsp;=&nbsp;false</td>
  <td class="infrulenamecol" rowspan="3">
    (E_WhileFalse) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">st&nbsp;=[&nbsp;WHILE&nbsp;b&nbsp;DO&nbsp;c&nbsp;END&nbsp;]=>&nbsp;st</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">beval&nbsp;st&nbsp;b&nbsp;=&nbsp;true</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">st&nbsp;=[&nbsp;c&nbsp;]=>&nbsp;st'</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">st'&nbsp;=[&nbsp;WHILE&nbsp;b&nbsp;DO&nbsp;c&nbsp;END&nbsp;]=>&nbsp;st''</td>
  <td class="infrulenamecol" rowspan="3">
    (E_WhileTrue) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">st&nbsp;&nbsp;=[&nbsp;WHILE&nbsp;b&nbsp;DO&nbsp;c&nbsp;END&nbsp;]=>&nbsp;st''</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

 下面是它的形式化定义。请确保你理解了它是如何与以上推理规则相对应的。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Reserved Notation</span> "st '=[' c ']⇒' st'"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">ceval</span> : <span class="id" type="var">com</span> → <span class="id" type="var">state</span> → <span class="id" type="var">state</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_Skip</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">SKIP</span> ]⇒ <span class="id" type="var">st</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_Ass</span>  : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">n</span> <span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span> = <span class="id" type="var">n</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span> ]⇒ (<span class="id" type="var">x</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">n</span> ; <span class="id" type="var">st</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_Seq</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">st''</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st'</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st''</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">c<sub>1</sub></span> ;; <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st''</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_IfTrue</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span> ]⇒ <span class="id" type="var">st'</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_IfFalse</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">false</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span> ]⇒ <span class="id" type="var">st'</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_WhileFalse</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">st</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">false</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_WhileTrue</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">st''</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st'</span> =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st''</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st''</span><br/>
<br/>
&nbsp;&nbsp;<span class="id" type="keyword">where</span> "st =[ c ]⇒ st'" := (<span class="id" type="var">ceval</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>).<br/>
</div>

<div class="doc">
将求值定义成关系而非函数的代价是，我们需要自己为某个程序求值成某种结束状态<b>构造证明</b>，
    而不能只是交给 Coq 的计算机制去做了。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">ceval_example1</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">empty_st</span> =[<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 2;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TEST</span> <span class="id" type="var">X</span> ≤ 1<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">THEN</span> <span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 3<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span> <span class="id" type="var">Z</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 4<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">FI</span><br/>
&nbsp;&nbsp;]⇒ (<span class="id" type="var">Z</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 4 ; <span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 2).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;我们必须提供中间状态&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Seq</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 2).<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;赋值指令&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;if&nbsp;指令&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfFalse</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab359"></a><h4 class="section">练习：2 星, standard (ceval_example2)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Example</span> <span class="id" type="var">ceval_example2</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">empty_st</span> =[<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0;; <span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 1;; <span class="id" type="var">Z</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 2<br/>
&nbsp;&nbsp;]⇒ (<span class="id" type="var">Z</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 2 ; <span class="id" type="var">Y</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 1 ; <span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 0).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab360"></a><h4 class="section">练习：3 星, standard, optional (pup_to_n)</h4>
 写一个 Imp 程序对从 <span class="inlinecode">1</span> 到 <span class="inlinecode"><span class="id" type="var">X</span></span> 进行求值（包括：将 <span class="inlinecode">1</span> <span class="inlinecode">+</span> <span class="inlinecode">2</span> <span class="inlinecode">+</span> <span class="inlinecode">...</span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">X</span></span>) 赋予变量 <span class="inlinecode"><span class="id" type="var">Y</span></span>。
   证明此程序对于 <span class="inlinecode"><span class="id" type="var">X</span></span> = <span class="inlinecode">2</span> 会按预期执行（这可能比你预想的还要棘手）。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">pup_to_n</span> : <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pup_to_2_ceval</span> :<br/>
&nbsp;&nbsp;(<span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 2) =[<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">pup_to_n</span><br/>
&nbsp;&nbsp;]⇒ (<span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 0 ; <span class="id" type="var">Y</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 3 ; <span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 1 ; <span class="id" type="var">Y</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 2 ; <span class="id" type="var">Y</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 0 ; <span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 2).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab361"></a><h2 class="section">求值的确定性</h2>

<div class="paragraph"> </div>

 将求值从计算式定义换成关系式定义是个不错的改变，
    因为它将我们从求值必须是全函数的人工需求中解放了出来。不过这仍然引发了一个问题：
    求值的第二种定义真的是一个偏函数吗？从同样的 <span class="inlinecode"><span class="id" type="var">st</span></span>
    开始, 我们是否有可能按照不同的方式对某个指令 <span class="inlinecode"><span class="id" type="var">c</span></span> 进行求值，
    从而到达两个不同的输出状态 <span class="inlinecode"><span class="id" type="var">st'</span></span> 和 <span class="inlinecode"><span class="id" type="var">st''</span></span>?

<div class="paragraph"> </div>

    实际上这不可能发生，因为 <span class="inlinecode"><span class="id" type="var">ceval</span></span> <b>确实</b>是一个偏函数： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>1</sub></span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st<sub>1</sub></span> = <span class="id" type="var">st<sub>2</sub></span>.<br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span> <span class="id" type="var">E<sub>1</sub></span> <span class="id" type="var">E<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">st<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">E<sub>1</sub></span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">st<sub>2</sub></span> <span class="id" type="var">E<sub>2</sub></span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">E<sub>2</sub></span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Skip&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Ass&nbsp;*)</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_Seq&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="comment">(*&nbsp;对断言的证明&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_1</span>; <span class="id" type="tactic">assumption</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_2</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_IfTrue，b<sub>1</sub>&nbsp;求值为&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_IfTrue，b<sub>1</sub>&nbsp;求值为&nbsp;false（矛盾）&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>5</sub></span>. <span class="id" type="tactic">discriminate</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_IfFalse,&nbsp;b<sub>1</sub>&nbsp;求值为&nbsp;true（矛盾）&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>5</sub></span>. <span class="id" type="tactic">discriminate</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_IfFalse，b<sub>1</sub>&nbsp;求值为&nbsp;false&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_WhileFalse，b<sub>1</sub>&nbsp;求值为&nbsp;false&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_WhileFalse，b<sub>1</sub>&nbsp;求值为&nbsp;true（矛盾）&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="tactic">discriminate</span> <span class="id" type="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_WhileTrue,&nbsp;b<sub>1</sub>&nbsp;求值为&nbsp;false（矛盾）&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>4</sub></span>. <span class="id" type="tactic">discriminate</span> <span class="id" type="var">H<sub>4</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_WhileTrue，b<sub>1</sub>&nbsp;求值为&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = <span class="id" type="var">st'0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">EQ<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="comment">(*&nbsp;对断言的证明&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_1</span>; <span class="id" type="tactic">assumption</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">subst</span> <span class="id" type="var">st'0</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHE1_2</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab362"></a><h1 class="section">对 Imp 进行推理</h1>

<div class="paragraph"> </div>

 我们会在<b>《编程语言基础》</b>中更加深入地探讨对 Imp 程序进行推理的系统性技术，
    不过目前只根据定义就能做很多工作。本节中会我们会探讨一些实例。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">plus2_spec</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">n</span> <span class="id" type="var">st'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> <span class="id" type="var">X</span> = <span class="id" type="var">n</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">plus2</span> ]⇒ <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st'</span> <span class="id" type="var">X</span> = <span class="id" type="var">n</span> + 2.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">st</span> <span class="id" type="var">n</span> <span class="id" type="var">st'</span> <span class="id" type="var">HX</span> <span class="id" type="var">Heval</span>.<br/>
</div>

<div class="doc">
反转 <span class="inlinecode"><span class="id" type="var">Heval</span></span> 实际上会强制让 Coq 展开 <span class="inlinecode"><span class="id" type="var">ceval</span></span> 求值的一个步骤 &mdash;
      由于 <span class="inlinecode"><span class="id" type="var">plus2</span></span> 是一个赋值，因此这种情况揭示了 <span class="inlinecode"><span class="id" type="var">st'</span></span> 一定是 <span class="inlinecode"><span class="id" type="var">st</span></span>
      通过新的值 <span class="inlinecode"><span class="id" type="var">X</span></span> 扩展而来的。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heval</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">clear</span> <span class="id" type="var">Heval</span>. <span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">t_update_eq</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab363"></a><h4 class="section">练习：3 星, standard, recommended (XtimesYinZ_spec)</h4>
 叙述并证明 <span class="inlinecode"><span class="id" type="var">XtimesYinZ</span></span> 的规范（Specification）。 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_XtimesYinZ_spec</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab364"></a><h4 class="section">练习：3 星, standard, recommended (loop_never_stops)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">loop_never_stops</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span>,<br/>
&nbsp;&nbsp;~(<span class="id" type="var">st</span> =[ <span class="id" type="var">loop</span> ]⇒ <span class="id" type="var">st'</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">contra</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">loop</span> <span class="id" type="keyword">in</span> <span class="id" type="var">contra</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">true</span> <span class="id" type="var">DO</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">END</span>)%<span class="id" type="var">imp</span> <span class="id" type="keyword">as</span> <span class="id" type="var">loopdef</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">eqn</span>:<span class="id" type="var">Heqloopdef</span>.<br/>
</div>

<div class="doc">
归纳讨论假设“<span class="inlinecode"><span class="id" type="var">loopdef</span></span> 会终止”之构造，其中多数情形的矛盾显而易见，
      可用 <span class="inlinecode"><span class="id" type="tactic">discriminate</span></span> 一步解决。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab365"></a><h4 class="section">练习：3 星, standard (no_whiles_eqv)</h4>
 考虑以下函数： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">no_whiles</span> (<span class="id" type="var">c</span> : <span class="id" type="var">com</span>) : <span class="id" type="var">bool</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">c</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">SKIP</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">true</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">_</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">_</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">true</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">c<sub>1</sub></span> ;; <span class="id" type="var">c<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">andb</span> (<span class="id" type="var">no_whiles</span> <span class="id" type="var">c<sub>1</sub></span>) (<span class="id" type="var">no_whiles</span> <span class="id" type="var">c<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">TEST</span> <span class="id" type="var">_</span> <span class="id" type="var">THEN</span> <span class="id" type="var">ct</span> <span class="id" type="var">ELSE</span> <span class="id" type="var">cf</span> <span class="id" type="var">FI</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">andb</span> (<span class="id" type="var">no_whiles</span> <span class="id" type="var">ct</span>) (<span class="id" type="var">no_whiles</span> <span class="id" type="var">cf</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">WHILE</span> <span class="id" type="var">_</span> <span class="id" type="var">DO</span> <span class="id" type="var">_</span> <span class="id" type="var">END</span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">false</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
<span class="id" type="var">Close</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span>.<br/>
</div>

<div class="doc">
此断言只对没有 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 循环的程序产生 <span class="inlinecode"><span class="id" type="var">true</span></span>。请用 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span>
    写出一个性质 <span class="inlinecode"><span class="id" type="var">no_whilesR</span></span> 使得 <span class="inlinecode"><span class="id" type="var">no_whilesR</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> 仅当 <span class="inlinecode"><span class="id" type="var">c</span></span> 是个没有
    <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 循环的程序时才可以证明。之后证明它与 <span class="inlinecode"><span class="id" type="var">no_whiles</span></span> 等价。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">no_whilesR</span>: <span class="id" type="var">com</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">no_whiles_eqv</span>:<br/>
&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span>, <span class="id" type="var">no_whiles</span> <span class="id" type="var">c</span> = <span class="id" type="var">true</span> ↔ <span class="id" type="var">no_whilesR</span> <span class="id" type="var">c</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab366"></a><h4 class="section">练习：4 星, standard (no_whiles_terminating)</h4>
 不涉及 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 循环的 Imp 程序一定会终止。请陈述并证明定理
    <span class="inlinecode"><span class="id" type="var">no_whiles_terminating</span></span> 来说明这一点。  按照你的偏好使用 <span class="inlinecode"><span class="id" type="var">no_whiles</span></span> 或 <span class="inlinecode"><span class="id" type="var">no_whilesR</span></span>。 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_no_whiles_terminating</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab367"></a><h1 class="section">附加练习</h1>

<div class="paragraph"> </div>

<a name="lab368"></a><h4 class="section">练习：3 星, standard (stack_compiler)</h4>
 旧式惠普计算器的编程语言类似于 Forth 和 Postscript，而其抽象机器类似于
    Java 虚拟机，即所有对算术表达式的求值都使用<b>栈</b>来进行。例如，表达式
<pre>
      (2*3)+(3*(4-2))
</pre>
   会被写成
<pre>
      2 3 * 3 4 2 - * +
</pre>
   的形式，其求值过程如下（右侧为被求值的程序，左侧为栈中的内容）：
<pre>
      [ ]           |    2 3 * 3 4 2 - * +
      [2]           |    3 * 3 4 2 - * +
      [3, 2]        |    * 3 4 2 - * +
      [6]           |    3 4 2 - * +
      [3, 6]        |    4 2 - * +
      [4, 3, 6]     |    2 - * +
      [2, 4, 3, 6]  |    - * +
      [2, 3, 6]     |    * +
      [6, 6]        |    +
      [12]          |
</pre>
  此练习的目的在于编写一个小型编译器，它将 <span class="inlinecode"><span class="id" type="var">aexp</span></span> 翻译成栈机器指令。

<div class="paragraph"> </div>

  栈语言的指令集由以下指令构成：

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">SPush</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>：将数 <span class="inlinecode"><span class="id" type="var">n</span></span> 压栈。

</li>
<li> <span class="inlinecode"><span class="id" type="var">SLoad</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span>：从存储中加载标识符 <span class="inlinecode"><span class="id" type="var">x</span></span> 并将其压栈。

</li>
<li> <span class="inlinecode"><span class="id" type="var">SPlus</span></span>：  从栈顶弹出两个数，将二者相加，并将其结果压栈。

</li>
<li> <span class="inlinecode"><span class="id" type="var">SMinus</span></span>： 类似，不过执行减法。

</li>
<li> <span class="inlinecode"><span class="id" type="var">SMult</span></span>：  类似，不过执行乘法。 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">sinstr</span> : <span class="id" type="keyword">Type</span> :=<br/>
| <span class="id" type="var">SPush</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>)<br/>
| <span class="id" type="var">SLoad</span> (<span class="id" type="var">x</span> : <span class="id" type="var">string</span>)<br/>
| <span class="id" type="var">SPlus</span><br/>
| <span class="id" type="var">SMinus</span><br/>
| <span class="id" type="var">SMult</span>.<br/>
</div>

<div class="doc">
请编写一个函数对栈语言程序进行求值。它应当接受一个状态、
    一个表示为数字列表的栈（栈顶项在表头），以及一个表示为指令列表的程序作为输入，
    并在程序执行后返回该栈。请在以下示例中测试你的函数。

<div class="paragraph"> </div>

    注意，当栈中的元素少于两个时，规范并未指定 <span class="inlinecode"><span class="id" type="var">SPlus</span></span>、<span class="inlinecode"><span class="id" type="var">SMinus</span></span> 或 <span class="inlinecode"><span class="id" type="var">SMult</span></span> 指令的行为。
    从某种意义上说，这样做并无必要，因为我们的编译器永远不会产生这种畸形的程序。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">s_execute</span> (<span class="id" type="var">st</span> : <span class="id" type="var">state</span>) (<span class="id" type="var">stack</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">prog</span> : <span class="id" type="var">list</span> <span class="id" type="var">sinstr</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">list</span> <span class="id" type="var">nat</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">s_execute1</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s_execute</span> <span class="id" type="var">empty_st</span> []<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">SPush</span> 5; <span class="id" type="var">SPush</span> 3; <span class="id" type="var">SPush</span> 1; <span class="id" type="var">SMinus</span>]<br/>
&nbsp;&nbsp;&nbsp;= [2; 5].<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">s_execute2</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s_execute</span> (<span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 3) [3;4]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">SPush</span> 4; <span class="id" type="var">SLoad</span> <span class="id" type="var">X</span>; <span class="id" type="var">SMult</span>; <span class="id" type="var">SPlus</span>]<br/>
&nbsp;&nbsp;&nbsp;= [15; 4].<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
接下来请编写一个将 <span class="inlinecode"><span class="id" type="var">aexp</span></span> 编译成栈机器程序的函数。运行此程序的效果
    应当和将该表达式的值压入栈中一致。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">s_compile</span> (<span class="id" type="var">e</span> : <span class="id" type="var">aexp</span>) : <span class="id" type="var">list</span> <span class="id" type="var">sinstr</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
在定义完 <span class="inlinecode"><span class="id" type="var">s_compile</span></span> 之后，请证明以下示例来测试它是否起作用。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">s_compile1</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">s_compile</span> (<span class="id" type="var">X</span> - (2 * <span class="id" type="var">Y</span>))%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;= [<span class="id" type="var">SLoad</span> <span class="id" type="var">X</span>; <span class="id" type="var">SPush</span> 2; <span class="id" type="var">SLoad</span> <span class="id" type="var">Y</span>; <span class="id" type="var">SMult</span>; <span class="id" type="var">SMinus</span>].<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab369"></a><h4 class="section">练习：4 星, advanced (stack_compiler_correct)</h4>
 现在我们将证明在之前练习中实现的编译器的正确性。记住当栈中的元素少于两个时，
    规范并未指定 <span class="inlinecode"><span class="id" type="var">SPlus</span></span>、<span class="inlinecode"><span class="id" type="var">SMinus</span></span> 或 <span class="inlinecode"><span class="id" type="var">SMult</span></span> 指令的行为。
    （为了让正确性证明更加容易，你可能需要返回去修改你的实现！）

<div class="paragraph"> </div>

    请证明以下定理。你需要先陈述一个更一般的引理来得到一个有用的归纳假设，
    由它的话主定理就只是一个简单的推论了。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">s_compile_correct</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">st</span> : <span class="id" type="var">state</span>) (<span class="id" type="var">e</span> : <span class="id" type="var">aexp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s_execute</span> <span class="id" type="var">st</span> [] (<span class="id" type="var">s_compile</span> <span class="id" type="var">e</span>) = [ <span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">e</span> ].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab370"></a><h4 class="section">练习：3 星, standard, optional (short_circuit)</h4>
 大部分现代编程语言对布尔 <span class="inlinecode"><span class="id" type="var">and</span></span> 运算提供了“短路求值”的方法：要对
    <span class="inlinecode"><span class="id" type="var">BAnd</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">b<sub>2</sub></span></span> 进行求值，首先对 <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> 求值。如果结果为 <span class="inlinecode"><span class="id" type="var">false</span></span>，那么整个
    <span class="inlinecode"><span class="id" type="var">BAnd</span></span> 表达式的求值就是 <span class="inlinecode"><span class="id" type="var">false</span></span>，而无需对 <span class="inlinecode"><span class="id" type="var">b<sub>2</sub></span></span> 求值。否则，<span class="inlinecode"><span class="id" type="var">b<sub>2</sub></span></span>
    的求值结果就决定了 <span class="inlinecode"><span class="id" type="var">BAnd</span></span> 表达式的值。

<div class="paragraph"> </div>

    请编写 <span class="inlinecode"><span class="id" type="var">beval</span></span> 的另一种版本，它能以这种方式对 <span class="inlinecode"><span class="id" type="var">BAnd</span></span> 执行短路求值，
    并证明它等价于 <span class="inlinecode"><span class="id" type="var">beval</span></span>。（注：二者等价只是因为 Imp 的表达式求值相当简单。
    在更大的语言中该表达式可能会发散，此时短路求值的 <span class="inlinecode"><span class="id" type="var">BAnd</span></span> <b>并不</b>
    等价于原始版本，因为它能让更多程序终止。） 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">BreakImp</span>.<br/>
</div>

<div class="doc">
<a name="lab371"></a><h4 class="section">练习：4 星, advanced (break_imp)</h4>
 像 C 和 Java 这样的指令式语言通常会包含 <span class="inlinecode"><span class="id" type="var">break</span></span> 或类似地语句来中断循环的执行。
    在本练习中，我们考虑如何为 Imp 加上 <span class="inlinecode"><span class="id" type="var">break</span></span>。首先，我们需要丰富语言的指令。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">com</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">CSkip</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CBreak</span>                        <span class="comment">(*&nbsp;&lt;---&nbsp;新增&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CAss</span> (<span class="id" type="var">x</span> : <span class="id" type="var">string</span>) (<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">CSeq</span> (<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">CIf</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) (<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">CWhile</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) (<span class="id" type="var">c</span> : <span class="id" type="var">com</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> "'SKIP'" :=<br/>
&nbsp;&nbsp;<span class="id" type="var">CSkip</span>.<br/>
<span class="id" type="keyword">Notation</span> "'BREAK'" :=<br/>
&nbsp;&nbsp;<span class="id" type="var">CBreak</span>.<br/>
<span class="id" type="keyword">Notation</span> "x '<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>' a" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CAss</span> <span class="id" type="var">x</span> <span class="id" type="var">a</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 60).<br/>
<span class="id" type="keyword">Notation</span> "c<sub>1</sub> ;; c<sub>2</sub>" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CSeq</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>).<br/>
<span class="id" type="keyword">Notation</span> "'WHILE' b 'DO' c 'END'" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CWhile</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>).<br/>
<span class="id" type="keyword">Notation</span> "'TEST' c<sub>1</sub> 'THEN' c<sub>2</sub> 'ELSE' c<sub>3</sub> 'FI'" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CIf</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>3</sub></span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>).<br/>
</div>

<div class="doc">
接着，我们需要定义 <span class="inlinecode"><span class="id" type="var">BREAK</span></span> 的行为。非形式化地说，只要 <span class="inlinecode"><span class="id" type="var">BREAK</span></span>
    在指令序列中执行，它就会终止该序列的执行并发出最内层围绕它的循环应当终止的信号。
    （如果没有任何围绕它的循环，那么就终止整个程序。）最终状态应当与
    <span class="inlinecode"><span class="id" type="var">BREAK</span></span> 语句执行后的状态相同。

<div class="paragraph"> </div>

    其要点之一在于当一个给定的 <span class="inlinecode"><span class="id" type="var">BREAK</span></span> 位于多个循环中时应该做什么。
    此时，<span class="inlinecode"><span class="id" type="var">BREAK</span></span> 应当只终止<b>最内层</b>的循环。因此，在执行完以下指令之后...

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;0;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">WHILE</span>&nbsp;~(0&nbsp;=&nbsp;<span class="id" type="var">Y</span>)&nbsp;<span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">WHILE</span>&nbsp;<span class="id" type="var">true</span>&nbsp;<span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">BREAK</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;-&nbsp;1<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>
<div class="paragraph"> </div>

</div>
    ...<span class="inlinecode"><span class="id" type="var">X</span></span> 的值应为 <span class="inlinecode">1</span> 而非 <span class="inlinecode">0</span>。

<div class="paragraph"> </div>

    表达这种行为的一种方式求值为求值关系添加一个形参，指定某个指令是否会执行
    <span class="inlinecode"><span class="id" type="var">BREAK</span></span> 语句： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">result</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">SContinue</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">SBreak</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Reserved Notation</span> "st '=[' c ']⇒' st' '/' s"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40, <span class="id" type="var">st'</span> <span class="id" type="tactic">at</span> <span class="id" type="var">next</span> <span class="id" type="var">level</span>).<br/>
</div>

<div class="doc">
直觉上说，<span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">s</span></span> 表示如果 <span class="inlinecode"><span class="id" type="var">c</span></span> 在 <span class="inlinecode"><span class="id" type="var">st</span></span> 状况下开始，
    它会在 <span class="inlinecode"><span class="id" type="var">st'</span></span> 状态下终止，围绕它的最内层循环（或整个程序）
    要么收到立即退出的信号（<span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">SBreak</span></span>），要么继续正常执行（<span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">SContinue</span></span>）。

<div class="paragraph"> </div>

    “<span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">s</span></span>”关系的定义非常类似于之前我们为一般求值关系
    （<span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>）给出的定义 &mdash; 我们只需要恰当地处理终止信号。

<div class="paragraph"> </div>

<ul class="doclist">
<li> 若指令为 <span class="inlinecode"><span class="id" type="var">SKIP</span></span>，则状态不变，任何围绕它的循环继续正常执行。

<div class="paragraph"> </div>


</li>
<li> 若指令为 <span class="inlinecode"><span class="id" type="var">BREAK</span></span>，则状态保持不变但发出 <span class="inlinecode"><span class="id" type="var">SBreak</span></span> 的信号。

<div class="paragraph"> </div>


</li>
<li> 若指令为赋值，则根据状态更新该变量绑定的值，并发出继续正常执行的信号。

<div class="paragraph"> </div>


</li>
<li> 若指令为 <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> 的形式，则按照 Imp 的原始语义更新状态，
      除此之外我们还要从被选择执行的分支中传播信号。

<div class="paragraph"> </div>


</li>
<li> 若指令为一系列 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode">;;</span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span>，我们首先执行 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span>。如果它产生了
      <span class="inlinecode"><span class="id" type="var">SBreak</span></span>，我们就跳过 <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> 的执行并将 <span class="inlinecode"><span class="id" type="var">SBreak</span></span> 的信号传给其外围的上下文中;
      结果状态与执行 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> 后获得的相同。否则，我们在执行完 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> 后的状态下执行
      <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> 并继续传递它产生的信号。

<div class="paragraph"> </div>


</li>
<li> 最后，对于形如 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> 的循环，其语义基本和此前相同。
      唯一的不同是，当 <span class="inlinecode"><span class="id" type="var">b</span></span> 求值为 <span class="inlinecode"><span class="id" type="var">true</span></span> 时执行 <span class="inlinecode"><span class="id" type="var">c</span></span> 并检查它产生的信号。
      若信号为 <span class="inlinecode"><span class="id" type="var">SContinue</span></span>，则按照原始语义继续执行。否则，我们终止此循环的执行，
      而其结果状态与当前迭代执行的结果相同。对于其它情况，由于 <span class="inlinecode"><span class="id" type="var">BREAK</span></span>
      只终止最内层的循环，因此 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 发出 <span class="inlinecode"><span class="id" type="var">SContinue</span></span> 的信号。 
</li>
</ul>

<div class="paragraph"> </div>

 基于以上描述，请完成 <span class="inlinecode"><span class="id" type="var">ceval</span></span> 关系的定义。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">ceval</span> : <span class="id" type="var">com</span> → <span class="id" type="var">state</span> → <span class="id" type="var">result</span> → <span class="id" type="var">state</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_Skip</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">CSkip</span> ]⇒ <span class="id" type="var">st</span> / <span class="id" type="var">SContinue</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
<br/>
&nbsp;&nbsp;<span class="id" type="keyword">where</span> "st '=[' c ']⇒' st' '/' s" := (<span class="id" type="var">ceval</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">s</span> <span class="id" type="var">st'</span>).<br/>
</div>

<div class="doc">
现在证明你定义的 <span class="inlinecode"><span class="id" type="var">ceval</span></span> 的如下性质： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">break_ignore</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">s</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">BREAK</span>;; <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st'</span> / <span class="id" type="var">s</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> = <span class="id" type="var">st'</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">while_continue</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">s</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st'</span> / <span class="id" type="var">s</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> = <span class="id" type="var">SContinue</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">while_stops_on_break</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st'</span> / <span class="id" type="var">SBreak</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st'</span> / <span class="id" type="var">SContinue</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab372"></a><h4 class="section">练习：3 星, advanced, optional (while_break_true)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">while_break_true</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st'</span> / <span class="id" type="var">SContinue</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st'</span> <span class="id" type="var">b</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">st''</span>, <span class="id" type="var">st''</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st'</span> / <span class="id" type="var">SBreak</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab373"></a><h4 class="section">练习：4 星, advanced, optional (ceval_deterministic)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ceval_deterministic</span>: <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">c</span>:<span class="id" type="var">com</span>) <span class="id" type="var">st</span> <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">st<sub>2</sub></span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>1</sub></span> / <span class="id" type="var">s<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st<sub>2</sub></span> / <span class="id" type="var">s<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st<sub>1</sub></span> = <span class="id" type="var">st<sub>2</sub></span> ∧ <span class="id" type="var">s<sub>1</sub></span> = <span class="id" type="var">s<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">
<span class="id" type="keyword">End</span> <span class="id" type="var">BreakImp</span>.<br/>
</div>

<div class="doc">
<a name="lab374"></a><h4 class="section">练习：4 星, standard, optional (add_for_loop)</h4>
 为该语言添加 C 风格的 <span class="inlinecode"><span class="id" type="keyword">for</span></span> 循环指令，更新 <span class="inlinecode"><span class="id" type="var">ceval</span></span> 的定义来定义
    <span class="inlinecode"><span class="id" type="keyword">for</span></span> 循环，按需添加 <span class="inlinecode"><span class="id" type="keyword">for</span></span> 循环的情况使得本文件中的所有证明都被
    Coq 所接受。

<div class="paragraph"> </div>

    <span class="inlinecode"><span class="id" type="keyword">for</span></span> 循环的参数应当包含 (a) 一个初始化执行的语句；
    (b) 一个在循环的每次迭代中都执行的测试，它决定了循环是否应当继续；
    (c) 一个在循环的每次迭代最后执行的语句，以及 (d) 一个创建循环体的语句
    （你不必关心为 <span class="inlinecode"><span class="id" type="keyword">for</span></span> 构造一个具体的记法，不过如果你喜欢，可以随意去做。） 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:24&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>